diff options
Diffstat (limited to 'math/glucose/files/patch-utils_System.cc')
| -rw-r--r-- | math/glucose/files/patch-utils_System.cc | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/math/glucose/files/patch-utils_System.cc b/math/glucose/files/patch-utils_System.cc new file mode 100644 index 000000000000..3a4d189a61f7 --- /dev/null +++ b/math/glucose/files/patch-utils_System.cc @@ -0,0 +1,11 @@ +--- utils/System.cc.orig 2018-02-01 09:11:32 UTC ++++ utils/System.cc +@@ -78,7 +78,7 @@ double Glucose::memUsed(void) { + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + return (double)ru.ru_maxrss / 1024; } +-double MiniSat::memUsedPeak(void) { return memUsed(); } ++//double MiniSat::memUsedPeak(void) { return memUsed(); } + + + #elif defined(__APPLE__) |