fix makefile.update_next_tag

This commit is contained in:
Simon Cruanes 2014-08-07 12:06:01 +02:00
parent c79fa08b52
commit 185cf14f28

View file

@ -57,10 +57,11 @@ push_stable: all
git push origin
git checkout master
VERSION=$(shell awk '/Version:/ {print $$2}' _oasis)
VERSION=$(shell awk '^/Version:/ {print $$2}' _oasis)
update_next_tag:
@echo "update version to $(VERSION)..."
sed -i "s/NEXT_VERSION/$(VERSION)/g" *.ml *.mli
sed -i "s/NEXT_RELEASE/$(VERSION)/g" *.ml *.mli
.PHONY: benchs tests examples update_next_tag push_doc push_stable