Merge bscpkgs into jungle #189

Manually merged
rarias merged 1013 commits from merge-bscpkgs into master 2025-10-07 16:12:34 +02:00
Showing only changes of commit d51fe5db48 - Show all commits

View File

@@ -76,6 +76,14 @@ checkExperiment() {
return 0
}
checkMountpoint() {
if [ ! -e "$garlicPrefix/garlic.control" ]; then
>&2 echo "error: missing $garlicPrefix/garlic.control"
>&2 echo "Is the mountpoint enabled?"
exit 1
fi
}
do_fetch() {
expName=$(basename $experiment)
user=$(ssh -G "$sshHost" | awk '/^user /{print $2}')
@@ -184,6 +192,8 @@ if [ -z "$trebuchet" ]; then
usage
fi
checkMountpoint
checkTrebuchet $trebuchet
experiment=$(findExperiment "$trebuchet")