diff options
-rw-r--r-- | utils/config.mlp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/utils/config.mlp b/utils/config.mlp index 33b8df934..630111f40 100644 --- a/utils/config.mlp +++ b/utils/config.mlp @@ -11,7 +11,7 @@ (* $Id$ *) -let version = "1.07+4" +let version = "1.07+5" let standard_library = try @@ -47,4 +47,3 @@ let system = "%%SYSTEM%%" let ext_obj = "%%EXT_OBJ%%" let ext_asm = "%%EXT_ASM%%" let ext_lib = "%%EXT_LIB%%" - |