#!/bin/sh
#
# On a roaming workstation, the local user's home directory is missing the .pki
# directory causing a question about the self-signed Debian Edu web server
# certificate if Chromium is used.
# Upon first login, a user can open a terminal window and execute this command
# to copy the whole PKI directory from the main server. 

# schweer, 2020-12-08

set -e
if [ -e /etc/debian-edu/config ] ; then
	. /etc/debian-edu/config
fi

if ! echo "$PROFILE" | grep -Eq 'Roaming-Workstation' ; then
		echo "This isn't a roaming workstation, nothing done."
	else
		if [ ! -d $HOME/.pki ] ; then
			scp -rq $USER@tjener:~/.pki $HOME
			echo "The PKI files have been copied from the main server."
		fi
fi