diff options
| author | Cyril Cohen | 2017-12-14 19:09:33 +0100 |
|---|---|---|
| committer | GitHub | 2017-12-14 19:09:33 +0100 |
| commit | 7ed910eed93cbd5523a731998b1d2c87db712b94 (patch) | |
| tree | 2b4fee8639328862336311f8f30e006a6644c219 /mathcomp/ssreflect/Makefile.coq-makefile | |
| parent | e4e5648250de1354366aa3b0637f8d6d72f5180f (diff) | |
| parent | 7406d43614dda186492f8e8cc184783980aaa969 (diff) | |
Merge pull request #155 from erikmd/fix/gh-61
Update v8.5 plugin to fix math-comp/math-comp#61
Diffstat (limited to 'mathcomp/ssreflect/Makefile.coq-makefile')
| -rw-r--r-- | mathcomp/ssreflect/Makefile.coq-makefile | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/Makefile.coq-makefile b/mathcomp/ssreflect/Makefile.coq-makefile index 68bfbc2..bf8115e 100644 --- a/mathcomp/ssreflect/Makefile.coq-makefile +++ b/mathcomp/ssreflect/Makefile.coq-makefile @@ -4,7 +4,8 @@ define coqmakefile MLLIB=;\ EXTRA=;\ case $(V) in\ - v8.5*|v8.4*)\ + v8.5*|v8.4*)\ + $$LN $(1)/plugin/$(V)/ssrmatching_plugin.mllib .;\ $$LN $(1)/plugin/$(V)/ssrmatching.mli .;\ $$LN $(1)/plugin/$(V)/ssrmatching.ml4 .;\ $$LN $(1)/plugin/$(V)/ssrmatching.v .;\ @@ -13,7 +14,7 @@ define coqmakefile $$LN $(1)/plugin/$(V)/ssrbool.v $(1)/;\ $$LN $(1)/plugin/$(V)/ssrfun.v $(1)/;\ $$LN $(1)/plugin/$(V)/ssreflect.v $(1)/;\ - MLLIB=ssreflect_plugin.mllib;\ + MLLIB="ssrmatching_plugin.mllib ssreflect_plugin.mllib";\ EXTRA="ssrmatching.mli ssrmatching.ml4 ssrmatching.v ssreflect.ml4";\ ;;\ v8.6*)\ |