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
