John, It appears the github repo is no longer synchronizing. I dcommitted some changes this morning (about 6 hours ago), but they don't show up on github. Can you check this ? Thanks, Geert