diff options
Diffstat (limited to 'tools/misc/Makefile.in')
| -rw-r--r-- | tools/misc/Makefile.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/misc/Makefile.in b/tools/misc/Makefile.in index b40ddd8..37a5cd8 100644 --- a/tools/misc/Makefile.in +++ b/tools/misc/Makefile.in @@ -318,7 +318,7 @@ MPE = @MPE@ MPI_GET_SIZE = @MPI_GET_SIZE@ MYAXE_LIBS = @MYAXE_LIBS@ MYIOD_LIBS = @MYIOD_LIBS@ -MYSHIPPER_LIBS = @MYSHIPPER_LIBS@ +MYMERCURY_LIBS = @MYMERCURY_LIBS@ NM = @NM@ NMEDIT = @NMEDIT@ OBJDUMP = @OBJDUMP@ |