Joris Vink 8aaf7aaf79 Alter where the version number comes from. ... Now if we are a git repo we fetch the branch name and commitid to build the version string. If there is no git repo we'll look at the RELEASE file.		2018-06-22 14:24:42 +02:00
..
Makefile	Alter where the version number comes from.	2018-06-22 14:24:42 +02:00