This is not urgent, but I'd prefer to remove the CodeMirror code from this repo. Then we have two options for fetching it:
- link to a CDN
- fetch a local copy
So far we've been using CDNs for almost everything, but either way I'd prefer to be consistent.
If we use local copies, we should add a Makefile that can fetch the required dependencies and unpack them. If we use local copies for CodeMirror, we might as well do the same for Bootstrap, jQuery, FontAwesome, and all our other dependenices.