8 Jun
2014
8 Jun
'14
5:52 p.m.
Hi, The develop branch of the super project was manually updated to use a more recent commit that hadn't been pushed to develop. Unfortunately my script for updating the super project doesn't check for this situation and could reset the library to the older version from develop at an arbitrary point (it doesn't normally because it's incremental, but occasionally a non-incremental run will set everything to the current develop branch). So I pushed the current revision to develop. It's just a merge commit that doesn't actually change any code, so I assume it was an oversight that it wasn't pushed. I hope that's okay. Daniel