The github repository was last updated a month ago whereas the SVN
repository has been updated many times this month.  Is the transfer of
updates to the SVN repository to the github repository supposed to be
automated?

	[[alternative HTML version deleted]]

