Small change to fix doc building on Debian

diff --git a/tools/linuxdoc b/tools/linuxdoc
index 045aa93b2df71893f6d540348cee1278c6276b7d..603a0bf53e88fe9ed161ed5c2bdaa21063403b13 100755 (executable)
--- a/tools/linuxdoc
+++ b/tools/linuxdoc
@@ -25,9 +25,13 @@ use FindBin;
 $prefix             = "/usr";
 $isoentities_prefix = "/usr";
 $DataDir            = "$FindBin::Bin/../doc/sbase";
-#$AuxBinDir          = "/usr/lib/linuxdoc-tools";
-$AuxBinDir          = "/usr/bin";
-
+if (-e "/usr/lib/linuxdoc-tools")
+{
+  $AuxBinDir          = "/usr/lib/linuxdoc-tools";
+} else
+{
+  $AuxBinDir          = "/usr/bin";
+}
 use lib "$FindBin::Bin/linuxdoc-tools";
 
 # ---------------------------------------------------------------------