From f377960d80f5a31620b1105758b0c24aef828cd3 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Mon, 12 Jun 2017 19:28:52 +0200 Subject: Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to generate them later. --- Makefile.build | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.build') diff --git a/Makefile.build b/Makefile.build index 2b0ef7aac..6e048ce94 100644 --- a/Makefile.build +++ b/Makefile.build @@ -95,7 +95,7 @@ plugins/micromega/certificate.cmx plugins/micromega/coq_micromega.cmx plugins/mi plugins/micromega/micromega.cmx plugins/micromega/micromega.cmo : plugins/micromega/micromega.cmi plugins/micromega/micromega.cmi : plugins/micromega/micromega.mli -plugins/micromega/micromega.mli plugins/micromega/micromega.ml : plugins/micromega/MExtraction.vo +plugins/micromega/generated_micromega.mli plugins/micromega/generated_micromega.ml : plugins/micromega/MExtraction.vo @: ########################################################################### -- cgit v1.2.3