* Make the devdocs more complete and self-contained
* Rename devdocs/misc-notes-from-contributors.md to devdocs/misc/misc_notes_for_committers.md
* Document the dependencies of the build script
* No need to manually make multiple commits
---------
Co-authored-by: Ian Butterworth <i.r.butterworth@gmail.com>