ports/ directory is listed in .gitignore, can't commit files to it

[allison]

The ports/ directory is listed in .gitignore because these files aren't shipped in the tarball. But, because they're in .gitignore, git won't allow updates for the files to be checked into the repository.

There was a semantic distinction lost here in the git migration, allowing files to be checked in, but not shipped in the tarball. I made a commit by temporarily removing ports/ from .gitignore, but we need a real fix.

[dukeleto]

You can commit files that are in .gitignore with

git add --force foo

I will add this to the git workflow document.