diff options
Diffstat (limited to 'lang/maude/files/patch-src__Mixfix__bottom.yy')
-rw-r--r-- | lang/maude/files/patch-src__Mixfix__bottom.yy | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/lang/maude/files/patch-src__Mixfix__bottom.yy b/lang/maude/files/patch-src__Mixfix__bottom.yy new file mode 100644 index 000000000000..5da5f16bd82f --- /dev/null +++ b/lang/maude/files/patch-src__Mixfix__bottom.yy @@ -0,0 +1,11 @@ +--- ./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); |