diff options
| author | Enrico Tassi | 2015-04-02 14:35:33 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-04-02 14:35:33 +0200 |
| commit | 9335bfaf04dfffa880f461392106f5c3b7f6ce16 (patch) | |
| tree | d8f6cc135df49fc124ca5f672c20c23e5e5ff748 /mathcomp/ssreflect/Makefile | |
| parent | 54d0e3b96cf06b8423e03d982d9c88fb50a21262 (diff) | |
support both coq.8.5beta1 and coq.8.5.dev
Diffstat (limited to 'mathcomp/ssreflect/Makefile')
| -rw-r--r-- | mathcomp/ssreflect/Makefile | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/mathcomp/ssreflect/Makefile b/mathcomp/ssreflect/Makefile index 6fd7ad0..fd8209d 100644 --- a/mathcomp/ssreflect/Makefile +++ b/mathcomp/ssreflect/Makefile @@ -4,12 +4,19 @@ ifeq "$(COQBIN)" "" COQBIN=$(dir $(shell which coqtop))/ endif +BRANCH_coq = $(shell $(COQBIN)/coqtop -v | head -1 | \ + sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/') + +HASH_coq = $(shell echo Quit. | $(COQBIN)/coqtop 2>&1 | \ + head -1 | sed 's/^.*(\([a-f0-9]*\).*/\1/') + +HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d -ifeq "$(shell $(COQBIN)/coqtop -v | head -1 | grep trunk | wc -l)" "1" -V=trunk + +ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)" +V=v8.5beta1 else -V=$(shell $(COQBIN)/coqtop -v | head -1 | \ - sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/') +V=$(BRANCH_coq) endif OLD_MAKEFLAGS:=$(MAKEFLAGS) @@ -19,10 +26,7 @@ MAKEFLAGS+=-B %: $(H)[ -e Makefile.coq ] || $(call coqmakefile) -# Override COQLIBS to find the "right" copy .ml files, otherwise -# coq_makefile uses only the -R in COQLIBS and ignores the -I in -# OCAMLLIBS to look for .ml files in order to generate .d files -# via coqdep + # Override COQDEP to find only the "right" copy .ml files $(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \ -f Makefile.coq $* \ COQDEP='$(COQBIN)/coqdep -exclude-dir plugin -c' |