playframework/Play20 — pull request #313 by blockmar (2012-05-15 11:04:40+00:00)
Title: Support for setting pid-file path using system propertie.

Added support for setting the pid-file location. (Using a system propertie)

Do we want it this way or do we want a possibility to name the the file like:

-Dpidfile.path=/tmp

or

-Dpidfile=/tmp/mypid

I implemented the -Dpidfile.path=/tmp solution.

(This replaces the old pull request from my master-branch.)