HoTT/HoTT — pull request #326 by JasonGross (2014-02-26 20:25:21+00:00)
Title: Use ${BASH_SOURCE[0]} instead of $0

Now we have better behavior when we use `source`; before we got the
parent's name, but now, we get the actual script's name.

Maybe we should also use the shorter version at http://stackoverflow.com/a/246128/377022 rather than the long `readlink -f` replacement we use now?

Anyway, I'm going to merge this once travis runs, because it's small and doesn't touch the actual library.