Skip to content
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

Possible issues on Windows due to 'aux' directory #111

Closed
maroneze opened this issue Jul 31, 2024 · 0 comments · Fixed by #119
Closed

Possible issues on Windows due to 'aux' directory #111

maroneze opened this issue Jul 31, 2024 · 0 comments · Fixed by #119

Comments

@maroneze
Copy link

Hello,

I just tried removing a Coq Windows-based installation on a test machine, and I had some weird errors related to the fact that, on Windows, names such as aux, con, etc, are handled in a special way due to old DOS-related reasons.

The cause was the aux folder present in ott, which was installed along with Coq.

Now, while Cygwin, Bash shell, and other programs can handle it, my Windows Explorer failed to, and Command Prompt required using special syntax (rd \\.\C:\...\ott.0.32\aux).

Now that I know about it, it's not an issue to me, but in case others might have this issue in the future, I'd just like to let you know about it. If you decide one day to do some refactoring, you might want to include renaming the directory by then.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant