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
>> component:
>>
>>    (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).

Great.

I now see change 3a9c2004b599 both on afp-2021 and afp-devel.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.