diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
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 @: ########################################################################### |