# HG changeset patch
# User Steve Huston <huston@srhuston.net>
# Date 1714147376 14400
# Node ID 02a3d7c46b2b7d1f13dd5db774e045855edf15b9
# Parent  61b830d340164f5bb1255a3237350d180b493af5
Better 'ds end' functionality, and ability to share a remote environment more easily

diff -r 61b830d34016 -r 02a3d7c46b2b .bash_aliases
--- 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"
diff -r 61b830d34016 -r 02a3d7c46b2b .shared/b
--- 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