diff options
| author | Cyril Cohen | 2018-07-31 15:20:43 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2018-07-31 15:41:45 +0200 |
| commit | 7d7b0688c818c5dde68d2b2bfc8ba3aecfe017d6 (patch) | |
| tree | 69c32570a9e238a717b89b5015137233d9080cbb /mathcomp/ssreflect/Makefile.detect-coq-version | |
| parent | 4199c23da311e612cb1ae45cf5519b5f3947c3b3 (diff) | |
removing dead code + reshuffling stuff
Diffstat (limited to 'mathcomp/ssreflect/Makefile.detect-coq-version')
| -rw-r--r-- | mathcomp/ssreflect/Makefile.detect-coq-version | 31 |
1 files changed, 13 insertions, 18 deletions
diff --git a/mathcomp/ssreflect/Makefile.detect-coq-version b/mathcomp/ssreflect/Makefile.detect-coq-version index 9c00aa3..385c078 100644 --- a/mathcomp/ssreflect/Makefile.detect-coq-version +++ b/mathcomp/ssreflect/Makefile.detect-coq-version @@ -1,25 +1,20 @@ -BRANCH_coq = $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \ +BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \ | wc -l | sed 's/ *//g') ifneq "$(BRANCH_coq)" "0" -BRANCH_coq = trunk +BRANCH_coq:= master else -BRANCH_coq = $(shell $(COQBIN)coqtop -v | head -1 \ - | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/') +BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 \ + | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/\1/') endif -HASH_coq = $(shell echo Quit. | $(COQBIN)coqtop 2>/dev/null | head -1 \ - | sed 's/^.*(\([a-f0-9]*\)).*/\1/' ) +V:=$(BRANCH_coq) -HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d -HASH_coq_v85beta2 = 94afd8996251c30d2188a75934487009538e1303 - -V=$(BRANCH_coq) -ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)" -V=v8.5beta1 -$(error "$(V) not supported: From X Require Y does not find X.Z.Y, use 8.4 or 8.5 > beta2") -endif -ifeq "$(HASH_coq)" "$(HASH_coq_v85beta2)" -V=v8.5beta2 -$(error "$(V) not supported: From X Require Y does not find X.Z.Y (in coqdep), use 8.4 or 8.5 > beta2") -endif +MLLIBEXTRA:=$(shell \ + if [ $(V) = "8.6" ];\ + then cp $(SSR)/plugin/v$(V)/ssreflect_plugin.mlpack .;\ + cp $(SSR)/plugin/v$(V)/ssreflect.ml4 .;\ + cp $(SSR)/plugin/v$(V)/ssrbool.v $(SSR)/;\ + cp $(SSR)/plugin/v$(V)/ssrfun.v $(SSR)/;\ + cp $(SSR)/plugin/v$(V)/ssreflect.v $(SSR)/;\ + echo "ssreflect_plugin.mlpack ssreflect.ml4"; fi) |
