Merge pull request #37358 from brainrape/idrisPackages-update

idrisPackages: add packages
2018-03-20 06:44:42 +00:00
parent c79cc60e64 23ee7c9d8d
commit 7bef35e691
82 changed files with 2427 additions and 57 deletions
@@ -626,6 +626,11 @@
    github = "bradediger";
    name = "Brad Ediger";
  };
+  brainrape = {
+    email = "martonboros@gmail.com";
+    github = "brainrape";
+    name = "Marton Boros";
+  };
  bramd = {
    email = "bram@bramd.nl";
    github = "bramd";