Browse Source

Fix make file to get release numbers safer

Carsten Dominik 10 years ago
parent
commit
b0844c5e74
1 changed files with 1 additions and 1 deletions
  1. 1 1
      Makefile

+ 1 - 1
Makefile

@@ -316,7 +316,7 @@ release:
 	git push -f origin maint
 	git checkout master
 	git merge -s ours maint
-	UTILITIES/set-version.pl -o $(TAG)
+	UTILITIES/set-version.pl -a $(TAG)
 	git commit -a -m "Update website to show $(TAG) as current release"
 	git push
 	make updateweb