On 12/03/2021 14:00, Peter Lammich wrote:
> On Fri, 2021-03-12 at 13:54 +0100, Manuel Eberl wrote:
>> Note that this is documented in ~~/README_REPOSITORY.
>
> Oh, I overlooked README_REPOSITORY. I checked README, but there is no
> reference to README_REPOSITORY in there, though it knows that it is a
> repository version!
The README is for releases, where README_REPOSITORY is actually absent.
I was hoping that the long and unusual name README_REPOSITORY makes it stick
out naturally --- and I keep pointing out that file frequently.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
