diff options
Diffstat (limited to 'Makefile.stage0')
| -rw-r--r-- | Makefile.stage0 | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/Makefile.stage0 b/Makefile.stage0 new file mode 100644 index 000000000..08aeaea37 --- /dev/null +++ b/Makefile.stage0 @@ -0,0 +1,16 @@ +####################################################################### +# 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.build + +.PHONY: stage0 +stage0: $(ML4FILES:.ml4=.ml4.d) + +##Somehow, make decides to delete the .ml4.d files if they are -include'd. +##This "stage0" hack to have them include'd, but no spurious error message +##on bootstrap. GNU Make bug suspected. |