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.