authorAxel Belinfante <Axel.Belinfante@cs.utwente.nl>
Fri, 28 Sep 2012 14:53:24 +0000 (16:53 +0200)
committerAxel Belinfante <Axel.Belinfante@cs.utwente.nl>
Fri, 28 Sep 2012 14:53:24 +0000 (16:53 +0200)
commitb2c7b6c16c15f6880f26ecf20e8a3a99ef9d0b1a
tree04e707c00ef5947f3b44e5b97843416a45ebb7a9
parent5bafc8e2520997e8c1b786cf551b4dbeed592246
use given cpu limit as soft limit; use 1.05 times higher value for cpu hard limit

without this, i.e. with cpu soft limit == cpu hard limit
a process is immediately killed when the limit is reached;
on linux, at least:
  - when the soft limit is reached, but the hard limit is not reached yet,
    (every second)  a special 'cpu time exceeded' signal is sent,
  - the process is only killed when the hard limit is reached

thus, with this change, on linux, we may get nicer error messages
(when process is run via a shell: 'CPU time limit exceeded', instead of 'Killed')
linux.c