changeset 92:17041a71bc02

maxtime is now auto-converted to maxcputime
author Oleg Oshmyan <chortos@inbox.lv>
date Mon, 28 Feb 2011 16:10:41 +0000
parents c62c9bfd614a
children bd3fc9017f91
files config.py
diffstat 1 files changed, 4 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/config.py	Mon Feb 28 16:05:20 2011 +0000
+++ b/config.py	Mon Feb 28 16:10:41 2011 +0000
@@ -123,6 +123,10 @@
 				module.paddummies = module.padwithzeroestolength[1]
 			except TypeError:
 				module.paddummies = module.padwithzeroestolength
+	if (not hasattr(module, 'maxcputime') and
+	    not hasattr(module, 'maxwalltime') and
+	    hasattr(module, 'maxtime')):
+		module.maxcputime = module.maxtime
 	for name in defaults_problem:
 		if not hasattr(globalconf, name):
 			setattr(module, name, getattr(module, name, defaults_problem[name]))