diff options
Diffstat (limited to 'src/c/Makefile.in')
| -rw-r--r-- | src/c/Makefile.in | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/c/Makefile.in b/src/c/Makefile.in index b9ff312e..a0bc1c32 100644 --- a/src/c/Makefile.in +++ b/src/c/Makefile.in @@ -154,6 +154,7 @@ MAKEINFO = @MAKEINFO@ MKDIR_P = @MKDIR_P@ MLLEX = @MLLEX@ MLTON = @MLTON@ +MLTONARGS = @MLTONARGS@ MLYACC = @MLYACC@ MSHEADER = @MSHEADER@ NM = @NM@ |