#!/bin/bash

# This script will be called before configuration files have been switched,
# with a command line argument of the name of the profile being applied.