Skip to content

Drop path when specifying out directory ? #5

@lemastero

Description

@lemastero

When compiling file with explicit existing directory name (app) I would expect it to succeed.

cabal run -- agda2rust ./test/Hello.agda -o app
Agda/Primitive.rs
test/Hello.rs
app/test/Hello.rs: withFile: does not exist (No such file or
directory)

Perhaps cabal run -- agda2rust ./test/Hello.agda -o app should generate output in app/Hello.rs not app/test/Hello.rs

Metadata

Metadata

Assignees

No one assigned

    Labels

    questionFurther information is requested

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions