Implement the '-strip' compiler option

[ghost]

This change allows users to choose whether or not to strip symbol
information from the output file. The fbc '-strip' option is analogous
to the ld '--strip-all' option.

This fixes issue #140.

[dkl]

Looks good to me. It would be useful to have changelog.txt entries for the new fbc options/behaviour changes.

[ghost]

Would you like me to add changelog.txt changes as part of this commit, or separate?

[dkl]

Ideally in the same commit.

[jayrm]

I agree. Ideally, updates to changelog.txt:

• in the same commit if the pull request is a single commit
• in the most recent commit (can be separate) if the pull request is multiple commits.

It is helpful to see updates to changelog.txt as part of the merge commit when merging the PR to master.

---

Not related specifically to this PR: a few of my thoughts follow, as I've been trying to take notice how we and github handle certain scenarios.

Whenever we have multiple pull requests on the go, we almost always get conflicts in changelog.txt. I have tried github's method to resolve conflicts on-the-fly: it works, but it does a merge master to PR, and triggers another Travis-CI build. Not the best in my opinion as it adds the extra merge commit just to resolve changelog.txt.

Rebase before merge seems like it should be OK in my opinion, resolving the conflicts locally. However, obviously must force push the new PR, and I haven't discovered the benefit of github keeping track of the force pushes yet. Also triggers another Travis-CI build.

A strategy for handling changelog.txt without conflict would be helpful. But I don't know what that strategy would be.

Regardless, git blame changelog.txt is a useful search method no matter where the changelog.txt gets updated, even directly on master branch, provided that updates are in same commit or immediately after the relevant commits made.

[ghost]

I've forced-pushed an updated commit with the changelog.txt changes.

Regarding your Github pull request workflow, it would be best to stick with the "Rebase and merge" option as it will keep the git history of the master branch clean without all the superfluous merge commit entries. This will benefit contributors looking back on the development history of the project, and ease debugging via git bisect operations and such.

The canonical way to achieve this in a pure git setup is to rebase on the local branch before fast-forwarding the master branch. In Github, this will create a new force-push entry, which triggers another Travis-CI build. Since the force-pushed commit after rebase would in theory be new -- the prescriptive context in the diff changed to accommodate the conflicting changelogs.txt of the other PR -- then another Travis-CI build would be warranted on the admittedly rare chance that some code was clobbered during the merge conflict resolution.

The reason force-pushes are tracked by Github is an extension of the Github site-wide philosophy of "always retain development history". It's the same reason why pull requests and issues are closed and not deleted. It's somewhat of a nuances to track obsolete force-pushes, but I think we're stuck with it unless Github changes its policy. Though it may be useful to have retained the force-push history if we end up with a situation where the merge conflict resolution introduces a bug by accident.

[jayrm]

Thanks. Fixes #140

Also, thanks for the helpful feedback on our workflow.