From 143c70bacc3298be2a48fe65cc669dfb2409c610 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 31 Oct 2018 14:29:19 +0100
Subject: fixing local Makefile should fix #238

---
 mathcomp/algebra/Makefile   |  8 ++------
 mathcomp/all/Makefile       | 22 ++--------------------
 mathcomp/character/Makefile |  7 ++-----
 mathcomp/field/Makefile     |  7 ++-----
 mathcomp/fingroup/Makefile  |  7 ++-----
 mathcomp/solvable/Makefile  |  7 ++-----
 6 files changed, 12 insertions(+), 46 deletions(-)

(limited to 'mathcomp')

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
-
-- 
cgit v1.2.3