diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-06-12 19:28:52 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-06-12 19:33:22 +0200 |
| commit | f377960d80f5a31620b1105758b0c24aef828cd3 (patch) | |
| tree | 2bb842c6645e62686f110e02912e8bcded6b5d2f /Makefile.build | |
| parent | 83d8b081c02cfde83c8fd93102f8f1aae3fe87b3 (diff) | |
Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to generate them later.
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 @: ########################################################################### |