changeset 274:02a3d7c46b2b

Better 'ds end' functionality, and ability to share a remote environment more easily
author Steve Huston <huston@srhuston.net>
date Fri, 26 Apr 2024 12:02:56 -0400
parents 61b830d34016
children 99368487ffe6
files .bash_aliases .shared/b
diffstat 2 files changed, 10 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/.bash_aliases	Thu Apr 25 16:38:37 2024 -0400
+++ b/.bash_aliases	Fri Apr 26 12:02:56 2024 -0400
@@ -58,7 +58,11 @@
   PIDFILE=${DOTHOME}/.dotshare-PID
 
   # If we want to kill an existing server, let's do that first.
-  if [ "$1" == "end" -a -e $PIDFILE ]; then
+  if [ "$1" == "end" ]; then
+    [[ -e $PIDFILE ]] || {
+      echo "No server detected"
+      return 1
+    }
     kill `cat $PIDFILE`
     unset DOTSHARE_PID DOTSHARE_PORT
     echo "Server terminated"
--- a/.shared/b	Thu Apr 25 16:38:37 2024 -0400
+++ b/.shared/b	Fri Apr 26 12:02:56 2024 -0400
@@ -21,5 +21,9 @@
   curl --create-dirs -so ${DOTHOME}/$F http://localhost:${DOTSHARE_PORT}/$F
 done
 
-export DOTHOME
+cat > ${DOTHOME}/.env-setup << EOF
+export DOTHOME=${DOTHOME}
 source ${DOTHOME}/shared_bashrc
+EOF
+
+source ${DOTHOME}/.env-setup