Emergency backup for documentation

Since the documentation we host on GitLab may not be available when something goes wrong, we should have independent backups which are available in an emergency.

GitLab Wikis are repositories, so we can clone them to our devices.

We should figure out what documentation we have and need, and create emergency backups.

• Identify all relevant documentation
• Create backups
• Ideally find a way to ensure that backups are kept up-to-date

For easier handling of wiki repos I created a small POSIX shell script. Running it makes sure that the latest version of all documentation repos specified at the bottom are available locally. Does not auto-update.:

#!/bin/sh

set -e

DOC_DIR="$(dirname "$(realpath "$0")")"

cd "$DOC_DIR"

update_repo() {
    REPO="$1"
    # shellcheck disable=SC2016
    REPO_DIR="$(echo "$REPO" | sed -E 's_^(.*/)+([^/]*)\.git$_\2_')"
    echo "$REPO_DIR"
    if [ -d "$DOC_DIR/$REPO_DIR" ]; then
        cd "$DOC_DIR/$REPO_DIR"
        git pull
        cd "$DOC_DIR"
    else
        git clone "$REPO"
    fi

}

update_repo git@sharing-codeability.uibk.ac.at:sharing/artemis-user-documentation.wiki.git
update_repo git@sharing-codeability.uibk.ac.at:sharing/codeability-sharing-platform.wiki.git