diff options
author | Wynn Wolf Arbor | 2020-05-28 18:38:04 +0200 |
---|---|---|
committer | Wynn Wolf Arbor | 2020-05-28 18:43:34 +0200 |
commit | a8207a5d773c514b07b555e256394b100c3df169 (patch) | |
tree | ba00d50d89030809161929da76068635e254bffb | |
parent | efdbb04b6799ea399cc9ca4f094b6b13fdb1c82f (diff) | |
download | skein-a8207a5d773c514b07b555e256394b100c3df169.tar.gz |
skein-infra: Rename mount point to repos.avail
Users might easily confuse the per-instance repos/ directory with the
mount point that contains all available repositories for a given user.
Therefore, be more clear about the purpose of the mount point and rename
it.
-rwxr-xr-x | skein-infra | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/skein-infra b/skein-infra index 2e8c866..850b980 100755 --- a/skein-infra +++ b/skein-infra @@ -52,10 +52,10 @@ setup() { git_repo_dir="${SKEIN_GIT_ROOT}/$user" test -d "$git_repo_dir" || continue - instance_repo_dir="$SKEIN_CGIT_ROOT"/home/$user/repos + available_repos="$SKEIN_CGIT_ROOT"/home/$user/repos.avail - bind_mount "$git_repo_dir" "$instance_repo_dir" - chmod 0701 "$instance_repo_dir" + bind_mount "$git_repo_dir" "$available_repos" + chmod 0701 "$available_repos" done } @@ -63,7 +63,7 @@ teardown() { rm "$SKEIN_CGIT_ROOT"/dev/null rmdir "$SKEIN_CGIT_ROOT"/dev - for i in "$SKEIN_CGIT_ROOT"/home/*/repos; do + for i in "$SKEIN_CGIT_ROOT"/home/*/repos.avail; do bind_umount "$i" done } |