diff --git a/src/Tools/mkroot_DOF b/src/Tools/mkroot_DOF index 8379184f..493c3d18 100755 --- a/src/Tools/mkroot_DOF +++ b/src/Tools/mkroot_DOF @@ -134,6 +134,7 @@ echo " \"preamble.tex\"" >> "$DIR"/ROOT echo " \"build\"" >> "$DIR"/ROOT sed -i -e "s/root.tex/isadof.cfg/" "$DIR"/ROOT sed -i -e "s/HOL/Isabelle_DOF/" "$DIR"/ROOT +sed -i -e "s/\"output\"\]/\"output\", document_build = dof\]/" "$DIR"/ROOT rm -f "$DIR"/document/root.tex # Creating isadof.cfg