aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/solvable
diff options
context:
space:
mode:
authorCyril Cohen2018-10-31 14:29:19 +0100
committerCyril Cohen2018-10-31 14:29:19 +0100
commit143c70bacc3298be2a48fe65cc669dfb2409c610 (patch)
tree884ae73a507a7e2af919b2a36f7c3da8e52c60ee /mathcomp/solvable
parentd6dc5741ba44808e5f2f01a238d972ec2c11737f (diff)
fixing local Makefile
should fix #238
Diffstat (limited to 'mathcomp/solvable')
-rw-r--r--mathcomp/solvable/Makefile7
1 files changed, 2 insertions, 5 deletions
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
-