diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common index 1be1d0dfb0..11cac44252 100644 --- a/Makefile.common +++ b/Makefile.common @@ -29,6 +29,11 @@ CHICKENOPT:=bin/coqchk.opt$(EXE) BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE) CHICKEN:=bin/coqchk$(EXE) +ifeq ($(HASNATDYNLINK),true) + DYNLINKCMXA:=dynlink.cmxa + NATDYNLINKDEF:=-DHasDynlink +endif + INSTALLBIN:=install INSTALLLIB:=install -m 644 MKDIR:=install -d |