#!/bin/sh
#
# switch to the specified developer version
#
# Author: Christian Starkjohann <cs@ds1.kph.tuwien.ac.at>
# Copyright: Public Domain
# There is absolutely no warranty etc., etc. .....
#

if [ "$1" = "3.2" -o "$1" = "4.0" ]; then
    rm -f /Dev-current
    ln -s "/Dev-$1" /Dev-current
else
    echo "usage: $0 <version>"
    echo "where <version> may be either 3.2 or 4.0"
fi