I thought I had committed this, but it's .gitignore'd. Add an exception to Ports/.gitignore and add it for real this time. :^) Fixes #5008.