diff options
| author | Enrico | 2018-10-31 15:45:01 +0100 |
|---|---|---|
| committer | GitHub | 2018-10-31 15:45:01 +0100 |
| commit | e3ded45b0d4f4d1667e99c8a7fac7d730e06c33e (patch) | |
| tree | 884ae73a507a7e2af919b2a36f7c3da8e52c60ee /mathcomp/field/Makefile | |
| parent | d6dc5741ba44808e5f2f01a238d972ec2c11737f (diff) | |
| parent | 143c70bacc3298be2a48fe65cc669dfb2409c610 (diff) | |
Merge pull request #239 from CohenCyril/Make_bug
fixing local Makefiles
Diffstat (limited to 'mathcomp/field/Makefile')
| -rw-r--r-- | mathcomp/field/Makefile | 7 |
1 files changed, 2 insertions, 5 deletions
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 - |