summaryrefslogtreecommitdiff
path: root/Makefile.stage3
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.stage3')
-rw-r--r--Makefile.stage321
1 files changed, 0 insertions, 21 deletions
diff --git a/Makefile.stage3 b/Makefile.stage3
deleted file mode 100644
index 1bd336d2..00000000
--- a/Makefile.stage3
+++ /dev/null
@@ -1,21 +0,0 @@
-#######################################################################
-# v # The Coq Proof Assistant / The Coq Development Team #
-# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay #
-# \VV/ #############################################################
-# // # This file is distributed under the terms of the #
-# # GNU Lesser General Public License Version 2.1 #
-#######################################################################
-
-include Makefile.stage2
-include Makefile.doc
-
--include $(VFILES:.v=.v.d)
-.SECONDARY: $(VFILES:.v=.v.d)
-
-.PHONY: stage3
-stage3: world
-
-# For emacs:
-# Local Variables:
-# mode: makefile
-# End: