26 Oct
2020
26 Oct
'20
2:43 p.m.
Hi Roberto, I fixed the problem. We recently changed the mirroring frequency from once every day, to once every hour. If you notice any issues please let me know. Best regards, Panos. On 10/26/20 3:16 PM, Roberto Cornacchia wrote:
Hello, I was wondering, is the syncing of the github repository mirror not scheduled?
I see that the latest commit on master is from today, but the latest commit on Oct2020 branch is from 14 days ago.
_______________________________________________ users-list mailing list users-list@monetdb.org https://www.monetdb.org/mailman/listinfo/users-list