From af8014da558755666f74f21bffb5b489a17fe6ba Mon Sep 17 00:00:00 2001
From: Ben Sima <ben@bsima.me>
Date: Fri, 10 Apr 2020 23:54:50 -0700
Subject: Make push work from anywhere

---
 push | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/push b/push
index 1fe9506..7c36684 100755
--- a/push
+++ b/push
@@ -1,5 +1,13 @@
 #!/usr/bin/env bash
-what=$(realpath "_bild/$1")
+set -ex
+prefix=$(echo $PWD | sed -e "s|^$BIZ_ROOT/*||g" -e "s|/|.|g")
+if [[ "$prefix" == "" ]]
+then
+  target="$1"
+else
+  target="$prefix.$1"
+fi
+what=$(realpath "$BIZ_ROOT/_bild/$target")
 where="$2"
 nix copy --to ssh://root@$where $what
 ssh root@$where $what/bin/switch-to-configuration switch
-- 
cgit v1.2.3