summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-02-11 11:29:36 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-02-11 11:29:36 -0500
commit3e839544936e8a9456d798d5f315991f976f6a53 (patch)
tree5000f3e2d50b46f7a0cb84380be457aba0fe2717 /src
parentabe2d7ed6e151579cd6f13fd0ce92e29bb83a23d (diff)
'configure' checks for libmhash and MLton
Diffstat (limited to 'src')
-rw-r--r--src/c/Makefile.in3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/c/Makefile.in b/src/c/Makefile.in
index c48ffb9f..98f431f9 100644
--- a/src/c/Makefile.in
+++ b/src/c/Makefile.in
@@ -145,6 +145,9 @@ LN_S = @LN_S@
LTLIBOBJS = @LTLIBOBJS@
MAKEINFO = @MAKEINFO@
MKDIR_P = @MKDIR_P@
+MLLEX = @MLLEX@
+MLTON = @MLTON@
+MLYACC = @MLYACC@
NM = @NM@
NMEDIT = @NMEDIT@
OBJDUMP = @OBJDUMP@