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
commit52971e912b15a083eb481361969ecd60e523c021 (patch)
tree5000f3e2d50b46f7a0cb84380be457aba0fe2717 /src
parenta91daf909f14d7bf3bd94cbec672497e1f23d400 (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@