aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-07-23 17:24:18 +0200
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-07-24 14:14:31 +0200
commitc15571e367cf4d75c9e4aac589170e0213e4fe3b (patch)
treeca12232b2b7c24d3e2a8e08491c6ca2c5da18034 /Makefile.common
parent1774a87504945a6e8b8aa465297dce672364b8a4 (diff)
fixup fakeide test-suite
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common1
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) \