-
Notifications
You must be signed in to change notification settings - Fork 3
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
How do I actually run it? #7
Comments
Also, one of the outputs seems to be the |
OK I kind of figured out how it works: basically, it needs Which turns out to be a problem on its own, because it means I can't re-run it on |
Yeah sorry, running this is very basic, but it didn't bother me so far... Here's how to run this after building it with
where Please note also that it makes no sense to run this with a single .webidl file, since many interfaces are spread across several files. |
And yes, the |
Ah, I missed that |
Because
idris2-dom
is missing IndexedDB support, I thought I'd just plop in the WebIDL files from e.g. https://searchfox.org/mozilla-central/source/dom/webidl and it should Just Work (tm), but alas, I can't even figure out how to run it. It seems to look for an.idr
output file in some directory somewhere (that I can kind-of override mostly with the-o
flag, if only I pass the-o
flag before the input file name?!), but I thought the whole point is to create the.idr
file.The text was updated successfully, but these errors were encountered: