On Apr 17, 2016, at 06:36 PM, Brian May wrote: >(or even better, use the quick-update script instead)
quick-update script? Oh, and +1 for the recommendation! I'd just add to also be sure that you commit and push your changes. ;) I've had one or two cases where the repo doesn't match the archive. <cough>dgit</cough> -Barry