[isabelle-dev] Bad documentation directory
makarius at sketis.net
Mon Feb 12 14:01:27 CET 2018
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:
> 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:
date: Fri Jan 19 14:55:46 2018 +0100
files: src/Pure/ML/ml_process.scala src/Pure/PIDE/protocol.ML
src/Pure/Tools/build.ML src/Pure/Tools/build.scala src/Pure/Tools/doc.scala
formal treatment of documentation names;
I've made it again more permissive here:
date: Mon Feb 12 13:27:30 2018 +0100
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.)
More information about the isabelle-dev