From af8014da558755666f74f21bffb5b489a17fe6ba Mon Sep 17 00:00:00 2001 From: Ben Sima Date: Fri, 10 Apr 2020 23:54:50 -0700 Subject: Make push work from anywhere --- push | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'push') 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