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
deprecate Cd command #16119
deprecate Cd command #16119
Conversation
@herbelin @SkySkimmer There was this plan to deprecate Cd entirely because it was only used in extraction. It might help with the output directory PR. If you disallow output directory and Cd to be used, it might simplofy the implementation. We can deprecate Cd as extraction can now have its output directory set IIRC. That was the only blocker. |
Oh I see that you've already seen this so nevermind then. |
@herbelin I won't have time to work on this so feel free to take over. I just wanted to make sure you knew about it. |
… Directory. New attempt to Alizter's PR coq#16119.
… Directory. New attempt to Alizter's PR coq#16119.
… Directory. New attempt to Alizter's PR coq#16119.
… Directory. New attempt to Alizter's PR coq#16119.
Keeping this as a draft for now. We need to provide output directory support for extraction first.