build-idris-package: ipkgName

2018-09-18 10:38:59 +02:00
parent 14d646edec
commit 7e0f7a0b54
23 changed files with 40 additions and 41 deletions
@@ -6,6 +6,8 @@ build-idris-package  {
  name = "vdom";
  version = "0.6.0";

+  ipkgName = "idris-vdom";
+
  src = fetchFromGitHub {
    owner = "brandondyck";
    repo = "idris-vdom";