Oh that is great news! Thanks! On Mon, 26 Oct 2020 at 15:54, Panagiotis Koutsourakis < panagiotis.koutsourakis@monetdbsolutions.com> wrote:
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
_______________________________________________ users-list mailing list users-list@monetdb.org https://www.monetdb.org/mailman/listinfo/users-list