Redirection should be followed by exit() immediately

[GoogleCodeExporter]

.. to make sure no other code is executed after the call.

Original issue reported on code.google.com by faj...@gmail.com on 29 Dec 2009 at 10:47

Attachments:

• redir.diff