From c15571e367cf4d75c9e4aac589170e0213e4fe3b Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Wed, 23 Jul 2014 17:24:18 +0200 Subject: fixup fakeide test-suite --- Makefile.common | 1 + 1 file changed, 1 insertion(+) (limited to 'Makefile.common') 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) \ -- cgit v1.2.3