diff options
| author | Eelco Dolstra <e.dolstra@tudelft.nl> | 2006-12-08 15:44:00 +0000 |
|---|---|---|
| committer | Eelco Dolstra <e.dolstra@tudelft.nl> | 2006-12-08 15:44:00 +0000 |
| commit | 9dbfe242e3bdbfc7728a36c8a2b9fbbea2c8ed68 (patch) | |
| tree | dc27874c617eabfa591ac32eca387de7e82835ae /doc | |
| parent | d3fe6ab024df7764f4de2a9dcf88e2daa981f786 (diff) | |
* Kill a build if it has gone for more than a certain number of
seconds without producing output on stdout or stderr (NIX-65). This
timeout can be specified using the `--max-silent-time' option or the
`build-max-silent-time' configuration setting. The default is
infinity (0).
* Fix a tricky race condition: if we kill the build user before the
child has done its setuid() to the build user uid, then it won't be
killed, and we'll potentially lock up in pid.wait(). So also send a
conventional kill to the child.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/manual/release-notes.xml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/manual/release-notes.xml b/doc/manual/release-notes.xml index a0b3ae68c..463337e8d 100644 --- a/doc/manual/release-notes.xml +++ b/doc/manual/release-notes.xml @@ -37,6 +37,11 @@ <listitem><para>TODO: magic <varname>exportReferencesGraph</varname> attribute.</para></listitem> + + <listitem><para>TODO: option <option>--max-silent-time</option>, + configuration setting + <literal>build-max-silent-time</literal>.</para></listitem> + </itemizedlist> |