[isabelle-dev] Repository OK?

[Amine Chaieb]

I think somebody removed Option.thy but left the dependency in the 
Makefile. This is strange since it is still needed by Extraction 
(Plain). theory Extraction imports Option ....

Amine.

Amine Chaieb wrote:
> Hi,
> 
> I updated and get the following error. What is Option?
> 
> Amine.
> 
> bash-3.2$ hg fetch
> Password:
> pulling from 
> ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle 
> 
> searching for changes
> adding changesets
> adding manifests
> adding file changes
> added 220 changesets with 900 changes to 440 files (+1 heads)
> updating to 30244:aea5d7fa7ef5
> 414 files updated, 0 files merged, 121 files removed, 0 files unresolved
> merging with 30024:f36741094f34
> 0 files updated, 0 files merged, 0 files removed, 0 files unresolved
> new changeset 30245:06b2d7f9f64b merges remote changes with local
> bash-3.2$ pwd
> /Users/ac638/tools/isabelle
> bash-3.2$ cd src/HOL
> bash-3.2$ isabelle make HOL-Library
> Building Pure ...
> Finished Pure (0:00:11 elapsed time, 0:00:07 cpu time, factor 0.63)
> make: *** No rule to make target `Option.thy', needed by 
> `/Users/ac638/.isabelle/heaps//polyml-5.2.1_x86-darwin/HOL'.  Stop.
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev