[isabelle-dev] Bad documentation directory

[Makarius]

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