8000 `Agda` package with missing data-files · Issue #62 · judah/pier · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content
Agda package with missing data-files #62
Open
@judah

Description

@judah

The Agda package is distributed on Hackage without its data-files. This leads to a build error with pier build Agda:

/private/var/folders/dk/xxrqcv1n5_5_gzkyzc94r5_80000gn/T/bR5j9VwncKwkZO0pqm7vFG2.Ssg14OGnc94Rr.yd3P0_75630/data-files/emacs-mode/*.el: fileAccess: does not exist (No such file or directory)

At least some of those files are generated by running agda-mode setup.

Not sure if we should just be more lenient with respect to data files, or else defer to #22.

Metadata

Metadata

Assignees

No one assigned

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions

      0