diff options
Diffstat (limited to 'lang/maude/files/patch-src__Mixfix__global.cc')
| -rw-r--r-- | lang/maude/files/patch-src__Mixfix__global.cc | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/lang/maude/files/patch-src__Mixfix__global.cc b/lang/maude/files/patch-src__Mixfix__global.cc new file mode 100644 index 000000000000..13d161784e77 --- /dev/null +++ b/lang/maude/files/patch-src__Mixfix__global.cc @@ -0,0 +1,14 @@ +--- ./src/Mixfix/global.cc.orig 2006-10-07 01:09:16.000000000 +0200 ++++ ./src/Mixfix/global.cc 2011-11-10 19:36:44.000000000 +0100 +@@ -89,6 +89,11 @@ + directory = executableDirectory; + return true; + } ++ if (directoryManager.checkAccess(MAUDE_DATADIR, fileName, R_OK, ext)) ++ { ++ directory = MAUDE_DATADIR; ++ return true; ++ } + } + else if (p + 1 < userFileName.length()) + { |