diff --git a/document-generator/Tools/DOF_mkroot b/document-generator/Tools/DOF_mkroot index 2791fed7..4cbd7836 100755 --- a/document-generator/Tools/DOF_mkroot +++ b/document-generator/Tools/DOF_mkroot @@ -143,7 +143,7 @@ if [ "$DOC" = true ]; then cp "$ISABELLE_HOME_USER/DOF/document-template/preamble.tex" "$DIR"/document/ cp "$ISABELLE_HOME_USER/DOF/document-template/ontologies.tex" "$DIR"/document/ for o in $ONTOLOGY; do - echo "\usepackage{$o}" >> "$DIR"/document/ontologies.tex; + echo "\usepackage{DOF-$o}" >> "$DIR"/document/ontologies.tex; done sed -e "s//$AUTHOR/" -e "s//$TITLE/" "$ISABELLE_HOME_USER/DOF/document-template/root-$TEMPLATE.tex" > "$DIR"/document/root.tex else