diff options
author | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-07-23 17:24:18 +0200 |
---|---|---|
committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-07-24 14:14:31 +0200 |
commit | c15571e367cf4d75c9e4aac589170e0213e4fe3b (patch) | |
tree | ca12232b2b7c24d3e2a8e08491c6ca2c5da18034 /Makefile.common | |
parent | 1774a87504945a6e8b8aa465297dce672364b8a4 (diff) |
fixup fakeide test-suite
Diffstat (limited to 'Makefile.common')
-rw-r--r-- | Makefile.common | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common index 4bc203197..f1817a956 100644 --- a/Makefile.common +++ b/Makefile.common @@ -54,6 +54,7 @@ endif BESTOBJ:=$(if $(OPT),.cmx,.cmo) BESTLIB:=$(if $(OPT),.cmxa,.cma) +BESTDYN:=$(if $(OPT),.cmxs,.cma) COQBINARIES:= $(COQMKTOP) \ $(COQTOPBYTE) $(COQTOPEXE) \ |