diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2012-12-12 16:42:15 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2012-12-12 16:42:15 -0500 |
| commit | 5005de069d5f7671ffac6e9d3e5833cc10b63cb0 (patch) | |
| tree | e4eba1ea9c294903b3ddd117830bda2267dfb8bb /src/c | |
| parent | ddeb9c57ed9b292082503aa10ebc942500ac8950 (diff) | |
Autogenerate some files
Diffstat (limited to 'src/c')
| -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@ |