aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/odd_order/Makefile
diff options
context:
space:
mode:
authorEnrico Tassi2018-04-17 16:57:13 +0200
committerEnrico Tassi2018-04-17 16:57:13 +0200
commiteaa90cf9520e43d0b05fc6431a479e6b9559ef0e (patch)
tree8499953a468a8d8be510dd0d60232cbd8984c1ec /mathcomp/odd_order/Makefile
parentc1ec9cd8e7e50f73159613c492aad4c6c40bc3aa (diff)
move odd_order to its own repository
Diffstat (limited to 'mathcomp/odd_order/Makefile')
-rw-r--r--mathcomp/odd_order/Makefile25
1 files changed, 0 insertions, 25 deletions
diff --git a/mathcomp/odd_order/Makefile b/mathcomp/odd_order/Makefile
deleted file mode 100644
index 14acb5c..0000000
--- a/mathcomp/odd_order/Makefile
+++ /dev/null
@@ -1,25 +0,0 @@
-H=@
-
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
-
-COQDEP=$(COQBIN)/coqdep
-
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
-
-.DEFAULT_GOAL := all
-
-%:
- $(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
- $(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
- -f Makefile.coq $* \
- COQDEP='$(COQDEP) -c'
-
-.PHONY: clean
-clean:
- $(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
- -f Makefile.coq clean
- $(H)rm -f Makefile.coq
-