diff options
Diffstat (limited to 'mathcomp/character/Makefile')
| -rw-r--r-- | mathcomp/character/Makefile | 7 |
1 files changed, 2 insertions, 5 deletions
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 - |