You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
If your source code is in src/sub and you add sourcedir = "src/sub" you will get unexpected '"' or with sourcedir = src/sub you will get unexpected '/'
Steps to Reproduce
Create a module called Main.idr in the directory issue/src
module Main
main : IO ()
main = pure ()
Create issue.ipkg in the parent directory of issue/src
package issue
modules = Main
sourcedir = idris/issue
run idris --build issue.ipkg
Expected Behavior
compilation completes
Observed Behavior
idris fails to parse ipkg file
The text was updated successfully, but these errors were encountered:
shmish111
added a commit
to shmish111/Idris-dev
that referenced
this issue
Dec 16, 2018
If your source code is in
src/sub
and you addsourcedir = "src/sub"
you will getunexpected '"'
or withsourcedir = src/sub
you will getunexpected '/'
Steps to Reproduce
Create a module called Main.idr in the directory
issue/src
Create issue.ipkg in the parent directory of
issue/src
run
idris --build issue.ipkg
Expected Behavior
compilation completes
Observed Behavior
idris fails to parse ipkg file
The text was updated successfully, but these errors were encountered: