From 4e67190ebee5d2ca241c5340a971ef340ce77ce7 Mon Sep 17 00:00:00 2001
From: Pavel 'LEdoian' Turinsky <ledoian@matfyz.cz>
Date: Sun, 2 Jan 2022 03:08:40 +0100
Subject: [PATCH] Add a simple script for remote deployment
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

It is really barebones and not much extensible…
---
 conf/remote.sh.inc | 13 +++++++++++++
 remote_deploy.sh   | 22 ++++++++++++++++++++++
 2 files changed, 35 insertions(+)
 create mode 100644 conf/remote.sh.inc
 create mode 100755 remote_deploy.sh

diff --git a/conf/remote.sh.inc b/conf/remote.sh.inc
new file mode 100644
index 0000000..907e050
--- /dev/null
+++ b/conf/remote.sh.inc
@@ -0,0 +1,13 @@
+#!/bin/echo Do not run
+
+# Config file for remote_deploy script
+# All values are required
+# This file is directly sourced from the script
+# Put this file to $XDG_CONFIG_DIR/wish/ and tweak.
+
+# Remote username
+USER=...
+# Host Wish is deployed on
+HOST=...
+# Remote directory containing this repository
+DIR=...
diff --git a/remote_deploy.sh b/remote_deploy.sh
new file mode 100755
index 0000000..7496dc8
--- /dev/null
+++ b/remote_deploy.sh
@@ -0,0 +1,22 @@
+#!/bin/sh
+
+set -eu
+
+if test -v XDG_CONFIG_DIR; then
+	CFGDIR="$XDG_CONFIG_DIR"
+else
+	CFGDIR="$HOME/.config"
+fi
+
+# Drop pre-existing values
+USER=
+HOST=
+DIR=
+
+. "$CFGDIR/wish/remote.sh.inc"
+
+ssh -l "$USER" "$HOST" -t "
+	set -eu
+	cd $DIR
+	./deploy.sh
+	"