From 185cf14f28d5eb3b23ac3e83016bb64629a1a9b1 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 7 Aug 2014 12:06:01 +0200
Subject: [PATCH] fix makefile.update_next_tag

---
 Makefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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