Tuj is also on GitHub now.

Even though there is not really much to manage, we decided to embrace the git tool. We should have downloaded the vanilla git rather than GitHub's Desktop GUI tool. Now the command line tools are located in a weird place in the system. We had to add that awkward thing to the PATH variable.

The gist is to just git verb it.

• Go to our homepage folder and git init it.
• Set up what to ignore in .gitignore. We explicitly added the *~ entry.
• Then git add everything. Those gitignored files will not be included.
• Then git commit with some comments.
• We set up the remote URI with the GUI. Supposedly we should have used git remote.
• Then we forcefully git push the stuff to remote. (Next time we can probably just git push without force.) It failed because we were behind a proxy...
• Set up proxy and push again. (Add entries like

[socks]
    proxy = socks5://someproxy:port
[http]
    proxy = http://someproxy:port
[https]
    proxy = https://someproxy:port

to the .gitconfig file in the home directory. Or git config it. We are no good with proxy. We have no idea which line actually worked.) Then everything went smoothly. It looked easy and nice. The code on our homepage ran and we were reminded of the good old days. Then naturally we cri. 😢

The end.

Update: our site is tainted by git now. 😱

Since we are not pushing to GitHub the git remote part is different. Normally one git remote add an ssh scheme. Then one git push there. However our network does not allow direct ssh connection.  There is a special session called Tuj2 already set up in PuTTY. It contains the info on that weird proxy and the private-public keys. We are supposed to just double click that and get connected. To make git know what to do when pushing, we need to do the following.

• Point the environment variable GIT_SSH to the plink binary. We have it with PuTTY.
• Tell git to push to remote ssh://Tuj2:/your-git-repository. Here Tuj2 is the name of the saved session. This is the key trick.

At this point we wondered if we should rename the session name or not and the '2' in the name irks us greatly. (Also before doing all this, set up git on server. Then set up the post-receive hook which git checkout the stuff into the web directory from which your web server serves pages.) After the git push is done, the site is updated automatically.

Side note: didn't dare to git checkout directly to the web directory. We made it git checkout to a test directory. It did work. Then we changed the checkout directory (given by the GIT_WORK_TREE variable) in the post-receive hook to the real thing. We are seriously worried now.

More detailed instruction can be found by Googling.