WIP: V20 current

Continuous state of V20.

Mainly so we can easily see and reference the history of commits.

To push change to here from V20, I do the following (after logging in to caress@exv20):

$ su nicos
$ set_gitlab_user mhart
$ cd /opt/nicos-core
$ git add [...]
$ git commit -m "Re #123 ..."
$ git push

set_gitlab_user is a convenience function defined in /home/nicos/set-git-user.sh.

You'll need to add your name and email there for it to work (where the "Add users here" comment is).

It is then equivalent to running (effect is local to the current terminal):

$ alias git="git -c user.name=\"User Name\" -c user.email=\"user@email.com\""

For the push to work, a proxy connection through the ESS tunnel must have been opened once since the last machine restart:

$ ssh -fND 7777 essuser@192.168.1.20

User/password must be someone's ESS credentials.