diff --git a/Makefile.dev b/Makefile.dev index 79ee11199b4421d304777d071dbfae1f97a420b9..38a26d991826fa319130d757a2f6fc5659a77faa 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -1,26 +1,4 @@ ####################################################################################### -# Workflow: -# C=make cia ; A=make amend ; U=make uv ; P=make opam-rel -# - to make sure the sha and the version are good, one should never -# do U and then A. -# - to make sure gtit is not confused, one should never do A and the P -# -# therefore, to avoid such problems, legal trace are defined by this automata: -# 0 -C-> 1 -# 1 -A-> 1 -# 1 -P-> 2 -# 2 -U-> 0 -# 1 -U-> 0 -# to implement such a workflow, C puts a lock (state 1) and U removes it (state 0) - - -############################### -# typical workflow: -# uv -> cia -> amend* -> push -> -# wait for gitlab release job -> pull (to get the release tag) -# and then; optionnaly, to release an opam version: -# opam-rel - ####################################################################################### @@ -54,46 +32,30 @@ README.md: README.txt ####################################################################################### # git entry points -####################################################################################### -# Workflow: -# C=git commit ; A=git amend ; U=update_version ; P=opam pack -# - to make sure the sha and the version are good, one should never -# do U and then A. -# - to make sure gtit is not confused, one should never do A and the P -# -# thereforeto avoid such problems, legal trace are defined by this automata: -# 0 -C-> 1 -# 1 -A-> 1 -# 1 -P-> 2 -# 2 -U-> 0 -# 1 -U-> 0 -# to implement such a workflow, C puts a lock (state 1) and U removes it (state 0) - uv:update_version update_version: git pull rm -f src/lv6version.ml make src/lv6version.ml +ifneq (,$(findstring -,$(VERSION))) + echo "won't update _oasis" +else cp _oasis _oasis.save cat _oasis.save | sed "s/^Version:.*/Version: $(VERSION)/" > _oasis - rm -f committed - git add _oasis - git add src/lv6version.ml make clean && make +endif BRANCH=$(shell git rev-parse --abbrev-ref HEAD) cia:test - test -f committed && \ - echo "*** I won't commit!\n*** until you 'make update_version'!" \ - || (git commit -a -F log && touch committed) && echo "Hint: 'make ci' to test the CI before doing 'make 'push'" + git commit -a -F log && echo "Hint: 'make ci' to test the CI before doing 'make 'push'" push: opam-test git push && make uv amend: - test -f committed && git commit -a -F log --amend + git commit -a -F log --amend ############################### diff --git a/Makefile.version b/Makefile.version new file mode 100644 index 0000000000000000000000000000000000000000..41bee0d8817b060a7b28c9821a889f2adfc39733 --- /dev/null +++ b/Makefile.version @@ -0,0 +1,14 @@ + +SHA:=$(shell git log -1 --pretty=format:"%h") +VERSION=$(shell git describe --tags) + +gen_version: + rm -f src/lv6version.ml + +src/lv6version.ml: Makefile + echo "(** Automatically generated from Makefile.version *) " > $@ + echo "let tool = \"lv6\"" >> $@ + echo "let str=\"$(VERSION)\"" >> $@ + echo "let sha=\"$(SHA)\"" >> $@ + echo "let branch = \"$(shell utils/get_branch_name)\"" >> $@ + echo "let maintainer = \"erwan.jahier@univ-grenoble-alpes.fr\"">> $@ diff --git a/src/lv6version.ml b/src/lv6version.ml deleted file mode 100644 index fb10147acff8fbd3029cd583bb350cd8ee062b2c..0000000000000000000000000000000000000000 --- a/src/lv6version.ml +++ /dev/null @@ -1,6 +0,0 @@ -(** Automatically generated from Makefile.version *) -let tool = "lv6" -let str="6.100.2" -let sha="44bc6b6" -let branch = "master" -let maintainer = "erwan.jahier@univ-grenoble-alpes.fr"