mount-robot: Configure for Michal S.

diff --git a/devel-utils/mount-robot b/devel-utils/mount-robot
index fad80655ee05d3fc500c580c0f774d456262fe84..0f890159e54cc31ef301bc1472e7cc1eebe69501 100755 (executable)
--- a/devel-utils/mount-robot
+++ b/devel-utils/mount-robot
@@ -8,6 +8,9 @@ if [ $USER = "zandar" ]; then
 elif [ $USER = "filip" ]; then
        mypath=/home/filip/fel/eb/build/ppc/_compiled
        mount_point=/home/filip
+elif [ $USER = "wsh" ]; then
+       mypath=/home/wsh/projects/eurobot/soft/build/ppc/_compiled
+       mount_point=/home/michal
 else
        echo "Error: Unknown user $USER" >&2
        exit 1