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

Paths given to the Windows setup script strip back slashes #45

Closed
MSoegtropIMC opened this issue Dec 15, 2020 · 1 comment
Closed

Paths given to the Windows setup script strip back slashes #45

MSoegtropIMC opened this issue Dec 15, 2020 · 1 comment
Labels
platform: windows Specific to windows
Milestone

Comments

@MSoegtropIMC
Copy link
Collaborator

The paths arguments given to the Windows setup script remove bask slashes - which is not common on Windows and a severe issue.

@MSoegtropIMC MSoegtropIMC added the platform: windows Specific to windows label Sep 25, 2021
@MSoegtropIMC MSoegtropIMC modified the milestones: 2022.03, 2022.03.1 Mar 21, 2022
@MSoegtropIMC MSoegtropIMC modified the milestones: 2022.03.1, 2022.09 Sep 13, 2022
@MSoegtropIMC
Copy link
Collaborator Author

Actually this only happens if the batch is called from cygwin bash, where back slashes are obviously stripped. It works fine when called from CMD, as

-destcyg=C:\bin\cygwin64_coq_platform ^
shows.

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

No branches or pull requests

1 participant