From 774750c2f73c87a9b35964b0882fec01fe714455 Mon Sep 17 00:00:00 2001
From: Egor Tensin <Egor.Tensin@gmail.com>
Date: Sat, 4 Mar 2023 10:13:48 +0100
Subject: fix_permissions.sh -> update.sh

Also, run links-update in addition with links-chmod.
---
 fix_permissions.sh | 18 ------------------
 update.sh          | 19 +++++++++++++++++++
 2 files changed, 19 insertions(+), 18 deletions(-)
 delete mode 100755 fix_permissions.sh
 create mode 100755 update.sh

diff --git a/fix_permissions.sh b/fix_permissions.sh
deleted file mode 100755
index 8506337..0000000
--- a/fix_permissions.sh
+++ /dev/null
@@ -1,18 +0,0 @@
-#!/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
-shopt -s inherit_errexit lastpipe
-
-script_dir="$( dirname -- "${BASH_SOURCE[0]}" )"
-script_dir="$( cd -- "$script_dir" && pwd )"
-readonly script_dir
-
-cd -- "$script_dir"
-export PATH="$script_dir/../config-links:$PATH"
-
-links-chmod go-w
diff --git a/update.sh b/update.sh
new file mode 100755
index 0000000..3dfc513
--- /dev/null
+++ b/update.sh
@@ -0,0 +1,19 @@
+#!/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
+shopt -s inherit_errexit lastpipe
+
+script_dir="$( dirname -- "${BASH_SOURCE[0]}" )"
+script_dir="$( cd -- "$script_dir" && pwd )"
+readonly script_dir
+
+export PATH="$script_dir/../config-links:$PATH"
+
+cd -- "$script_dir"
+links-update
+links-chmod go-w
-- 
cgit v1.2.3