PERMISSIONS

#!/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-2.0"

tail -2 "$0" | ssh git@laragit.epfl.ch setperms ${thisrepo}

exit $_

# **Do not** add new lines after the following two!
WRITERS kuncak psuter rblanc edarulov hojjat ekneuss kandhada kuraj gvero
READERS @lara mazimmer hardy amin