Skip to content

Automatically trim whitespace in vscode - #788

Merged
mattam82 merged 1 commit into
coq-8.16from
vscode-auto-trim-whitespace
Nov 28, 2022
Merged

Automatically trim whitespace in vscode#788
mattam82 merged 1 commit into
coq-8.16from
vscode-auto-trim-whitespace

Conversation

@yforster

Copy link
Copy Markdown
Member

Should be merged only after #773

@mattam82
mattam82 merged commit 44aabad into coq-8.16 Nov 28, 2022
@TheoWinterhalter
TheoWinterhalter deleted the vscode-auto-trim-whitespace branch November 28, 2022 21:08
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.

2 participants