Recent update of GitLab brought renaming of several things. Most notably for us, Issues were generalized into Work items. We will try to update the materials to reflect the new naming as soon as possible.

Each student has access to the following repository (as usual, LOGIN is your CAS/SIS login).

gitolite3@linux.ms.mff.cuni.cz:config-LOGIN

This repository is initially empty but it can be used to store your common configuration of Shell and Git that you want to share across multiple machines.

Such configuration typically includes things like

  • setting your editor (i.e., $EDITOR),
  • setting common ls aliases,
  • setting Git identity (git config ...) or
  • defining Git aliases (e.g. git ll).

Machine linux.ms.mff.cuni.cz is setup in such way that if you clone this repository into your $HOME as my-config, it will automatically load your shell (Bash) and Git configuration.

git clone gitolite3@linux.ms.mff.cuni.cz:config-LOGIN my-config

For that to happen, you need to store your Bash configuration into file bashrc (notice that this is not a hidden file) and your Git configuration into gitconfig (again, a normal file) inside your config-LOGIN repository.

The same will apply during exams: if you clone the config-LOGIN repository into $HOME/my-config inside your temporary (examination) accounts, your Bash and Git configuration will be automatically loaded.

(Unfortunately, the automatic loading does not apply to your normal school accounts where you need to add it manually. But only once so it is well worth the effort.)

Of course, you have to open a new shell after setting up bashrc to see the new configuration working there. It also means that you can check that it is working in the new terminal (or SSH session, or window of tmux, etc.), and if not, repair it in the old one, which still uses the old configuration. The Git configuration is loaded on each git command execution and is thus applied immediately.

You can also store your notes into the config-LOGIN repository so that you do not need to print them. Do not store there anything that might be contrary to the course rules (this includes, for example, AI agents or exam solutions from your colleagues). Also, please, keep the repository small (under 5MB). Thank you.

Example contents of bashrc file

The following is a typical contents of bashrc in your config-LOGIN repository.


# Editor configuration (e.g., for git commit)
export EDITOR=mcedit

# Common aliases
alias ls='ls -F --color=auto'
alias ll='ls -l'

# Prompt should include machine name
PS1='\u@\h \w\$'
Do not copy your full .bashrc into my-config/bashrc. You will most likely cause an endless loop (see below)!

Example contents of gitconfig file

The following is a typical contents of gitconfig in your config-LOGIN repository.

Look into your current ~/.gitconfig to see which aliases you have defined and feel free to copy from there.

[alias]
	st = status
	ci = commit
	br = branch
	co = checkout
	sw = switch
	ll = log --format='tformat:%C(yellow)%h%Creset %an (%cr) %C(yellow)%s%Creset' --max-count=20 --first-parent

Using on other machines than linux.ms.mff.cuni.cz

As stated above, when config-LOGIN is cloned into ~/my-config on linux.ms, your Bash and Git configuration will be loaded automatically.

If you want to use the same setup for your own machines (e.g., your notebook), the following will show you how. We highly recommend you do this because it will allow you to share your common configuration across multiple machines. It will make you more productive. And it is super cool too :-).

Modifications of ~/.bashrc

The following should be placed int your existing ~/.bashrc file so that it also includes your configuration from ~/my-config.

if [ -f "$HOME/my-config/bashrc" ] && [ -r "$HOME/my-config/bashrc" ]; then
    . "$HOME/my-config/bashrc"
fi

With this snippet in place (that checks that $HOME/my-config/bashrc is a readable file and then includes it), it is no longer necessary to, for example, set your aliases and $EDITOR directly in ~/.bashrc but keep it in the reusable config-LOGIN repository.

Do NOT insert the code above (or similar) into your my-config/bashrc as it will lead to an endless loop during Bash startup.

On a remote machine that might prevent you from logging in (and it will probably look like a network error from the outside), eventually blocking you because it will look like an unsuccesfull attempt for a login.

(If you managed to do that, edit your files outside of Shell. If you managed to do that on the remote machine, please, file a confidential issue and we will try to fix it for you.)

Modifications of ~/.gitconfig

The following should be placed into your ~/.gitconfig where Git can pick it up.

[include]
	path = ~/my-config/gitconfig

Note that this will work even if the ~/my-config/gitconfig file does not exist (Git will silently ignore it).