huge merge

[Radu Grigore]

I did a big merge. Let me know what I broke.

One thing I noticed is that Mike added some command line flags that
look like they conflict (semantically) with some older changes from my
fork that I didn't merge. I'll look into this by tomorrow.

Story: I used to merge the master branch into my fork regularly, but I
stopped during the summer. That led to a huge number of conflicts [1].
I fixed them superficially, because I thought this is better than
letting things get even more out-of-sync. I'll be coding these days so
I hope I'll fix whatever I broke.

[1] http://github.com/rgrig/jstar/commit/0d98eaf9a16cf1dc82ccf539f3477d8179c7e387