Important to note that we're only ever teaching the students to run these commands on the server, where they should have the same environment as us (the OS of their personal computer is irrelevant -- the server runs Linux).

So rather than adding instructions for each OS, we maybe just add a note somewhere that the commands can be different on different OSes. Although I think we already have a note like this in chapter 2's section about editing config files.