diff --git a/Makefile.dev b/Makefile.dev index 0efdc125fab6570cfb8b9863bfc9e68bd33e8ec3..cb0366a61e4ccf475fd03b6eedd27da798d2757a 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -32,7 +32,11 @@ update_version: rm -f src/lutilsVersion.ml make src/lutilsVersion.ml cp _oasis _oasis.save +ifneq (,$(findstring -,$(VERSION))) + echo "won't update _oasis" +else cat _oasis.save | sed "s/^Version:.*/Version: $(VERSION)/" > _oasis +endif rm -f committed make clean && make diff --git a/Makefile.version b/Makefile.version new file mode 100644 index 0000000000000000000000000000000000000000..f3e2c02e7f77d28d7b89772631f63bc1fe32779c --- /dev/null +++ b/Makefile.version @@ -0,0 +1,15 @@ + +SHA:=$(shell git log -1 --pretty=format:"%h") + +# Both work. Which one is the best? +VERSION=$(shell ./node_modules/.bin/git-latest-semver-tag) +VERSION=$(shell git describe --tags) + +del_version: + rm -f src/lutilsVersion.ml + +gen_version: del_version src/lutilsVersion.ml + +src/lutilsVersion.ml: + echo "let str=\"$(VERSION)\"" > src/lutilsVersion.ml ; \ + echo "let sha=\"$(SHA)\"" >> src/lutilsVersion.ml diff --git a/doc/version.tex b/doc/version.tex deleted file mode 100644 index 8add3d8ad65be2524a49826023afbafaa8c0de0d..0000000000000000000000000000000000000000 --- a/doc/version.tex +++ /dev/null @@ -1,4 +0,0 @@ -\newcommand{\version}{1.48.4} -\newcommand{\sha}{d90fc9d} -\newcommand{\versionname}{none} -\newcommand{\versiondate}{28-01-19} diff --git a/src/lutilsVersion.ml b/src/lutilsVersion.ml deleted file mode 100644 index 2ac792b8bfc5728b005d55a0ac72ac747cf147d9..0000000000000000000000000000000000000000 --- a/src/lutilsVersion.ml +++ /dev/null @@ -1,2 +0,0 @@ -let str="1.48.4" -let sha="d90fc9d"