diff options
Diffstat (limited to '')
| -rw-r--r-- | lang/maude/files/patch-src__Mixfix__commands.yy | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/lang/maude/files/patch-src__Mixfix__commands.yy b/lang/maude/files/patch-src__Mixfix__commands.yy deleted file mode 100644 index c5ee2ba8312b..000000000000 --- a/lang/maude/files/patch-src__Mixfix__commands.yy +++ /dev/null @@ -1,17 +0,0 @@ ---- ./src/Mixfix/commands.yy.orig 2014-09-03 02:51:54.000000000 +0200 -+++ ./src/Mixfix/commands.yy 2014-09-03 02:53:05.000000000 +0200 -@@ -23,12 +23,12 @@ - /* - * Commands. - */ --command : KW_SELECT { lexBubble(END_COMMAND, 1) } -+command : KW_SELECT { lexBubble(END_COMMAND, 1); } - endBubble - { - interpreter.setCurrentModule(lexerBubble); - } -- | KW_DUMP { lexBubble(END_COMMAND, 1) } -+ | KW_DUMP { lexBubble(END_COMMAND, 1); } - endBubble - { - if (interpreter.setCurrentModule(lexerBubble)) |