diff options
| author | Cyril Cohen | 2018-10-31 14:29:19 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2018-10-31 14:29:19 +0100 |
| commit | 143c70bacc3298be2a48fe65cc669dfb2409c610 (patch) | |
| tree | 884ae73a507a7e2af919b2a36f7c3da8e52c60ee /mathcomp | |
| parent | d6dc5741ba44808e5f2f01a238d972ec2c11737f (diff) | |
fixing local Makefile
should fix #238
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/Makefile | 8 | ||||
| -rw-r--r-- | mathcomp/all/Makefile | 22 | ||||
| -rw-r--r-- | mathcomp/character/Makefile | 7 | ||||
| -rw-r--r-- | mathcomp/field/Makefile | 7 | ||||
| -rw-r--r-- | mathcomp/fingroup/Makefile | 7 | ||||
| -rw-r--r-- | mathcomp/solvable/Makefile | 7 |
6 files changed, 12 insertions, 46 deletions
diff --git a/mathcomp/algebra/Makefile b/mathcomp/algebra/Makefile index 47dd8b4..23d9c98 100644 --- a/mathcomp/algebra/Makefile +++ b/mathcomp/algebra/Makefile @@ -1,10 +1,6 @@ # -*- Makefile -*- -COQPROJECT="Make" - -# -------------------------------------------------------------------- -include ../Makefile.common - -# -------------------------------------------------------------------- +COQPROJECT=Make COQMAKEOPTIONS=--no-print-directory +include ../Makefile.common diff --git a/mathcomp/all/Makefile b/mathcomp/all/Makefile index 30204d2..7e434c0 100644 --- a/mathcomp/all/Makefile +++ b/mathcomp/all/Makefile @@ -1,25 +1,7 @@ # -*- Makefile -*- -COQPROJECT="Make" - -# -------------------------------------------------------------------- -include Makefile.common - -# -------------------------------------------------------------------- +COQPROJECT=Make COQMAKEOPTIONS=--no-print-directory # -------------------------------------------------------------------- -.PHONY: install - -install: - $(MAKE) -f Makefile.coq install - -# -------------------------------------------------------------------- -.PHONY: count - -COQFILES := $(shell grep '.v$$' Make) - -count: - @coqwc $(COQFILES) | tail -1 | \ - awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}' - +include ../Makefile.common diff --git a/mathcomp/character/Makefile b/mathcomp/character/Makefile index 47dd8b4..7e434c0 100644 --- a/mathcomp/character/Makefile +++ b/mathcomp/character/Makefile @@ -1,10 +1,7 @@ # -*- Makefile -*- -COQPROJECT="Make" +COQPROJECT=Make +COQMAKEOPTIONS=--no-print-directory # -------------------------------------------------------------------- include ../Makefile.common - -# -------------------------------------------------------------------- -COQMAKEOPTIONS=--no-print-directory - diff --git a/mathcomp/field/Makefile b/mathcomp/field/Makefile index 47dd8b4..7e434c0 100644 --- a/mathcomp/field/Makefile +++ b/mathcomp/field/Makefile @@ -1,10 +1,7 @@ # -*- Makefile -*- -COQPROJECT="Make" +COQPROJECT=Make +COQMAKEOPTIONS=--no-print-directory # -------------------------------------------------------------------- include ../Makefile.common - -# -------------------------------------------------------------------- -COQMAKEOPTIONS=--no-print-directory - diff --git a/mathcomp/fingroup/Makefile b/mathcomp/fingroup/Makefile index 47dd8b4..7e434c0 100644 --- a/mathcomp/fingroup/Makefile +++ b/mathcomp/fingroup/Makefile @@ -1,10 +1,7 @@ # -*- Makefile -*- -COQPROJECT="Make" +COQPROJECT=Make +COQMAKEOPTIONS=--no-print-directory # -------------------------------------------------------------------- include ../Makefile.common - -# -------------------------------------------------------------------- -COQMAKEOPTIONS=--no-print-directory - diff --git a/mathcomp/solvable/Makefile b/mathcomp/solvable/Makefile index 47dd8b4..7e434c0 100644 --- a/mathcomp/solvable/Makefile +++ b/mathcomp/solvable/Makefile @@ -1,10 +1,7 @@ # -*- Makefile -*- -COQPROJECT="Make" +COQPROJECT=Make +COQMAKEOPTIONS=--no-print-directory # -------------------------------------------------------------------- include ../Makefile.common - -# -------------------------------------------------------------------- -COQMAKEOPTIONS=--no-print-directory - |