diff options
| author | Enrico Tassi | 2015-04-02 14:02:15 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-04-02 14:02:15 +0200 |
| commit | 46330661210f8e535179cf837fe4b53de9133571 (patch) | |
| tree | 3ecc47239d1504aca52c91f21c43b85259766101 /mathcomp | |
| parent | e2530e78deda5cf6be2111951efb8ea747af7fa8 (diff) | |
The right way to ignore the plugin directory
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/Makefile b/mathcomp/ssreflect/Makefile index 12c71fc..6fd7ad0 100644 --- a/mathcomp/ssreflect/Makefile +++ b/mathcomp/ssreflect/Makefile @@ -25,7 +25,7 @@ MAKEFLAGS+=-B # via coqdep $(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \ -f Makefile.coq $* \ - COQLIBS='-I . -R . mathcomp.ssreflect' + COQDEP='$(COQBIN)/coqdep -exclude-dir plugin -c' define coqmakefile (echo "Generating Makefile.coq for Coq $(V) with COQBIN=$(COQBIN)";\ |