diff --git a/PERMISSIONS b/PERMISSIONS new file mode 100755 index 0000000000000000000000000000000000000000..83cbe2125032421b2884445d90d646c2d82a0962 --- /dev/null +++ b/PERMISSIONS @@ -0,0 +1,16 @@ +#!/bin/bash + +# Just editing this file won't affect the permissions. After editing it, you +# also need to execute it. +# +# The creator of this repository is psuter. + +thisrepo="projects/leon-kaplan" + +tail -2 "$0" | ssh git@laragit.epfl.ch setperms ${thisrepo} + +exit $_ + +# **Do not** add new lines after the following two! +WRITERS kuncak psuter +READERS megard