-
Notifications
You must be signed in to change notification settings - Fork 11
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
_oasis_remove_.ml and OASIS version of setup.ml #30
Comments
Good remark. Since I use the OASIS lib, I guess it is possible to have that info from the library, right? |
I could detect that because the |
No. This is embedded into one of the record field deep inside the auto-generated setup.ml. This is actually unfortunate, because I know it would be useful to auto-extract it, without running setup.ml.
|
I used 2. because I would prefer not to have to trust the setup.ml file. :-) |
Pre-emptive bug, I don't yet have the issue.
I see in commit 77b07e3, that you have removed the generation of oasis_remove.ml (which is a good thing).
The problem is that '-C' is only fixed with OASIS 0.4.7 and you may have a setup.ml generated with former version (e.g. 0.4.6).
Can you check the version of OASIS used to generate setup.ml and issue an error if < 0.4.7 ?
To check the version
The text was updated successfully, but these errors were encountered: