diff --git a/docs/upload b/docs/upload new file mode 100755 index 0000000000000000000000000000000000000000..37ef364af2bea6626ffa1120a0b96f3054da9cc4 --- /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 +