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
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
> - Jenkins
> - (shell access to) lxcisa0
Jenkins is back online. For technical reasons, lxcisa0 will only become
available again tomorrow.
Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
