diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index 08ae6f8358..5c8c28cd31 100644 --- a/Makefile.common +++ b/Makefile.common @@ -111,7 +111,9 @@ REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) # Object and Source files ########################################################################### -LIBCOQRUN:=kernel/byterun/libcoqrun.a +COQRUN := coqrun +LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a +DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN).so CLIBS:=unix.cma |