gcc/DATESTAMP not updated any longer

[Martin Liška]

On 12/11/20 2:17 PM, Rainer Orth wrote:
> Rainer Orth <ro@CeBiTec.Uni-Bielefeld.DE> writes:
> 
>> I noticed that gcc/DATESTAMP isn't updated any longer after this
>> Friday.  I doubt this is intentional...
> 
> This has happened again tonight...
> 
> 	Rainer
> 

Thanks for heads up. I'm aware of it and I don't see reason why (running the
update script in dry mode works).

@Jakub: Can you please take a look?

Thanks,
Martin