On 12/02/18 10:52, Lars Hupel wrote: > When I clone a fresh copy of Isabelle, or run "hg clean --all", then > "isabelle build" fails with the following error message: > > *** Bad documentation directory: > "/home/lars/work/isabelle/src/Tools/jEdit/dist/doc" > > That directory is not present by default and appears to be only created > by "isabelle jedit". A workaround is to always run "isabelle jedit -bf" > before running "isabelle build".
That is a consequence of the formal treatment of documentation names here: changeset: 67462:bddfa23a4ea9 user: wenzelm date: Fri Jan 19 14:55:46 2018 +0100 files: src/Pure/ML/ml_process.scala src/Pure/PIDE/protocol.ML src/Pure/PIDE/protocol.scala src/Pure/PIDE/resources.ML src/Pure/Thy/document_antiquotations.ML src/Pure/Thy/sessions.scala src/Pure/Tools/build.ML src/Pure/Tools/build.scala src/Pure/Tools/doc.scala description: formal treatment of documentation names; I've made it again more permissive here: changeset: 67604:02cf352cbc4c tag: tip user: wenzelm date: Mon Feb 12 13:27:30 2018 +0100 files: src/Pure/Tools/doc.scala description: permissive Doc.dirs: some entries may be absent due to distribution bootstrap, e.g. $JEDIT_HOME/dist/doc; That is for merely convenience when experimenting with a few sessions from a cloned repository. A formal test does require "isabelle jedit -b" before "isabelle build -a". (That is implicit in the order given in README_REPOSITORY and explicit in the build_history tool.) Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev