diff options
| -rw-r--r-- | .gitattributes | 1 | ||||
| -rw-r--r-- | .gitcommit | 1 | ||||
| -rw-r--r-- | src/base/main/mainReal.c | 4 |
3 files changed, 4 insertions, 2 deletions
diff --git a/.gitattributes b/.gitattributes index 400b529f..93b5c864 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1,3 +1,4 @@ +/.gitcommit export-subst * text=auto *.c text diff --git a/.gitcommit b/.gitcommit new file mode 100644 index 00000000..46b7856f --- /dev/null +++ b/.gitcommit @@ -0,0 +1 @@ +$Format:%h$ diff --git a/src/base/main/mainReal.c b/src/base/main/mainReal.c index a13be5e5..420f2cf1 100644 --- a/src/base/main/mainReal.c +++ b/src/base/main/mainReal.c @@ -134,7 +134,7 @@ int Abc_RealMain( int argc, char * argv[] ) break; case 'm': { -#if !defined(WIN32) && !defined(__wasm) +#if !defined(WIN32) && !defined(ABC_NO_RLIMIT) int maxMb = atoi(globalUtilOptarg); printf("Limiting memory use to %d MB\n", maxMb); struct rlimit limit = { @@ -146,7 +146,7 @@ int Abc_RealMain( int argc, char * argv[] ) break; } case 'l': { -#if !defined(WIN32) && !defined(__wasm) +#if !defined(WIN32) && !defined(ABC_NO_RLIMIT) rlim_t maxTime = atoi(globalUtilOptarg); printf("Limiting time to %d seconds\n", (int)maxTime); struct rlimit limit = { |