diff options
Diffstat (limited to 'tools/Makefile.shared')
| -rw-r--r-- | tools/Makefile.shared | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/Makefile.shared b/tools/Makefile.shared index 8fd3c9435e..2b19278486 100644 --- a/tools/Makefile.shared +++ b/tools/Makefile.shared @@ -264,7 +264,7 @@ opnames.ml: ../byterun/instruct.h sed -e '/\/\*/d' \ -e '/^#/d' \ -e 's/enum \(.*\) {/let names_of_\1 = [|/' \ - -e 's/};$$/ |]/' \ + -e 's/.*};$$/ |]/' \ -e 's/\([A-Z][A-Z_0-9a-z]*\)/"\1"/g' \ -e 's/,/;/g' \ ../byterun/instruct.h > opnames.ml |