diff options
| -rwxr-xr-x | fix_permissions.sh | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/fix_permissions.sh b/fix_permissions.sh index ff0489b..8223002 100755 --- a/fix_permissions.sh +++ b/fix_permissions.sh @@ -1,7 +1,14 @@ #!/usr/bin/env bash +# Some utilities (for example, ssh) fix too relaxed file permissions +# automatically. +# Others (GHCi is the reason this script exists) just spit out a warning and +# ignore such files. +# This script simply removes the write permission for everybody except myself +# for every file in this repository. + set -o errexit -o nounset -o pipefail script_dir="$( dirname -- "${BASH_SOURCE[0]}" )" script_dir="$( cd -- "$script_dir" && pwd )" -find "$script_dir" -mindepth 1 -path "$script_dir/.git" -prune -o -exec chmod g-w {} + +find "$script_dir" -mindepth 1 -path "$script_dir/.git" -prune -o -exec chmod go-w {} + |