changeset 159:d0cdc3f47182

oops we already had a zsh enabling .profile
author Dirk Olmes <dirk@xanthippe.ping.de>
date Sat, 14 Dec 2019 06:17:27 +0100
parents 08620c68ca55
children c35d56590441
files .profile-zsh profile
diffstat 2 files changed, 4 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/.profile-zsh	Sat Dec 14 06:13:05 2019 +0100
+++ b/.profile-zsh	Sat Dec 14 06:17:27 2019 +0100
@@ -1,4 +1,8 @@
+#
+# Use this as .profile on systems where the default shell cannot be changed to zsh
+#
 if [ ! -z "$SSH_TTY" ]; then
+	# this is an interactive shell, replace the current shell with a zsh
     if [ -f /bin/zsh ]; then
         export SHELL=/bin/zsh
         exec /bin/zsh -l
--- a/profile	Sat Dec 14 06:13:05 2019 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-#
-# Use this as .profile on systems where the default shell cannot be changed to zsh
-#
-if [ ! -z "$SSH_TTY" ]; then
-	# this is an interactive shell, replace the current shell with a zsh
-    if [ -f /bin/zsh ]; then
-        export SHELL=/bin/zsh
-        exec /bin/zsh -l
-    fi
-fi