diff options
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) \ |