diff options
Diffstat (limited to '')
| -rw-r--r-- | lang/maude/files/patch-src__Mixfix__bottom.yy | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/lang/maude/files/patch-src__Mixfix__bottom.yy b/lang/maude/files/patch-src__Mixfix__bottom.yy deleted file mode 100644 index 5da5f16bd82f..000000000000 --- a/lang/maude/files/patch-src__Mixfix__bottom.yy +++ /dev/null @@ -1,11 +0,0 @@ ---- ./src/Mixfix/bottom.yy.orig 2014-09-03 02:49:14.000000000 +0200 -+++ ./src/Mixfix/bottom.yy 2014-09-03 02:50:56.000000000 +0200 -@@ -23,7 +23,7 @@ - %% - - static void --yyerror(char *s) -+yyerror(UserLevelRewritingContext::ParseResult *parseResult, char *s) - { - if (!(UserLevelRewritingContext::interrupted())) - IssueWarning(LineNumber(lineNumber) << ": " << s); |