diff --git a/Makefile b/Makefile index ce1e9de..db135ee 100644 --- a/Makefile +++ b/Makefile @@ -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