Adds gerschtli to maintainer-list

2018-05-17 14:20:28 -05:00
parent bd648f321c
commit d9266340e1
1 changed files with 5 additions and 0 deletions
@@ -1483,6 +1483,11 @@
    github = "georgewhewell";
    name = "George Whewell";
  };
+  gerschtli = {
+    email = "tobias.happ@gmx.de";
+    github = "Gerschtli";
+    name = "Tobias Happ";
+  };
  gilligan = {
    email = "tobias.pflug@gmail.com";
    github = "gilligan";