Skip to content

updates to devcontainer in templates#1106

Merged
oscarlevin merged 1 commit intomainfrom
devcontainer
Dec 31, 2025
Merged

updates to devcontainer in templates#1106
oscarlevin merged 1 commit intomainfrom
devcontainer

Conversation

@oscarlevin
Copy link
Member

This improves the devcontainer for templates, including turning off property suggestions (that come through via the redhat xml extension and are duplicated by pretext-tools), removes the install-sage script, and improves the install-pandoc script. In particular, it will close #1073.

@oscarlevin oscarlevin merged commit 0d3a018 into main Dec 31, 2025
6 checks passed
@oscarlevin oscarlevin deleted the devcontainer branch December 31, 2025 03:57
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.

devcontainer cannot not use sudo

1 participant