Re: [isabelle] The instructions in AFP's "Using Entries" do not work
On 06/06/2021 02:35, Gerwin Klein wrote:
>> (2) Be more ambitious in having the AFP/thys/etc/settings initialize
>> $AFP_BASE if not yet done by the user. Thus users get two choices for AFP as
>> (a) use component AFP, but not AFP/thys; thus the important "isabelle
>> build -a" versus "isabelle build -a -d '$AFP'" works properly
>> (b) use component AFP/thys and let its etc/settings init AFP if required
>> (otherwise users would have to init both AFP and AFP/thys manually).
> This is much better than my solution, and I'd be very happy with it.
>> This is a long explanation for a small change, see the attachment for afp-2021
>> (and merge into afp-devel).
I now see change 3a9c2004b599 both on afp-2021 and afp-devel.
This archive was generated by a fusion of
Pipermail (Mailman edition) and