Lucas Bickel 854110cb73 Get rid of what I am sure is dead in dev_tools

2017-03-18 12:21:25 +01:00

..

release.sh

Fix tag checkout during release

2017-03-15 17:07:52 +01:00