playframework/Play20 — pull request #342 by benmccann (2012-05-31 06:00:31+00:00)
Title: Add an option for enabling/disabling the pid file.

I'd like the disable the RUNNING_PID file. I have my own server management with its own pid file (I'm using supervisor - see supervisord.org). It can be advantageous for this functionality to be external to the server because it's then possible to deal with the case where server exists abnormally. Having this check is interfering with supervisor.