--- /dev/null
+#!/bin/sh
+# 2019-09-10, Nico Schottelius, Seoul
+
+if [ $# -ne 1 ]; then
+ echo "$0: <webserver directory>"
+ echo 'Export your friends to the web!'
+ exit 1
+fi
+
+dir=$1; shift
+keys="$dir/rifkeys"
+
+gpg -a --export RIF > "$keys"
+
+# Ensure everyone can read them
+chmod 0644 "$keys"