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

[VsCoq1] [.vscodeignore] Simplify ignore rules #176

Closed
wants to merge 1 commit into from
Closed

[VsCoq1] [.vscodeignore] Simplify ignore rules #176

wants to merge 1 commit into from

Conversation

artagnon
Copy link

We just need to move client/{snippets, syntaxes} to the root directory,
and then we can ignore all of client/.

We just need to move client/{snippets, syntaxes, coq.configuration.json}
to the root directory, and then we can ignore all of client/.
@artagnon
Copy link
Author

@fakusb Could you review this? Thanks.

@fakusb
Copy link

fakusb commented Mar 15, 2021

Does this make your workflow easier or is it "tidy up"-work? I was under the impression of it beeing the later, and was afraid I might break things I don't test when including it in the most recent release.

@artagnon
Copy link
Author

Yes, it's more tidy-up work. Do test it first.

@maximedenes maximedenes changed the title [.vscodeignore] Simplify ignore rules [VsCoq1] [.vscodeignore] Simplify ignore rules Feb 14, 2023
@thery
Copy link
Contributor

thery commented Mar 1, 2023

This is superseded by #411

@thery thery closed this Mar 1, 2023
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 this pull request may close these issues.

3 participants