diff -r 5db67376df7d -r c587f5ac4a98 lib/Tools/mkdir
--- a/lib/Tools/mkdir	Mon Feb 14 20:43:12 2000 +0100
+++ b/lib/Tools/mkdir	Mon Feb 14 20:49:08 2000 +0100
@@ -87,15 +87,21 @@
 
 # IsaMakefile
 
+DOCUMENT_ROOT=""
+
 if [ -n "$BUILD" ]; then
   IMAGES="$NAME"
   TEST=""
   TARGET="\$(OUT)/$NAME"
+  ROOT_ML="ROOT.ML"
+  [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="document/root.tex"
   USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library"
 else
   IMAGES=""
   TEST="$NAME"
   TARGET="\$(LOG)/$LOGIC-$NAME.gz"
+  ROOT_ML="$NAME/ROOT.ML"
+  [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="$NAME/document/root.tex"
   USEDIR="\$(USEDIR)"
 fi
 
@@ -128,12 +134,12 @@
       echo "$LOGIC:"
       echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC"
       echo
-      echo "$TARGET: \$(OUT)/$LOGIC     ## add $NAME sources here"
+      echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT  ## add $NAME sources here"
       echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
     else
       echo "$NAME: $TARGET"
       echo
-      echo "$TARGET:                    ## add $NAME sources here"
+      echo "$TARGET: $ROOT_ML $DOCUMENT_ROOT  ## add $NAME sources here"
       echo -e "\t@$USEDIR $LOGIC $NAME"
     fi
     echo