From 2038efcbc05d9dd85b50070efbf08da0cc9fcfd8 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 14 Dec 2017 13:57:12 +0100 Subject: [PATCH] add upload script --- docs/upload | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100755 docs/upload diff --git a/docs/upload b/docs/upload new file mode 100755 index 000000000..37ef364af --- /dev/null +++ b/docs/upload @@ -0,0 +1,7 @@ +#!/bin/sh +set -e +cd "$(dirname "$(readlink -e "$0")")" + +rub iris +scp iris.pdf mpi-contact:plv.mpi-sws.org/iris/appendix-3.1.pdf + -- GitLab