Skip to content
This repository has been archived by the owner on Aug 29, 2023. It is now read-only.

fix(install_debian): don't install VSCode if VSCodium has been installed #161

Merged
merged 1 commit into from
Feb 22, 2023

Conversation

Hagb
Copy link
Contributor

@Hagb Hagb commented Jan 19, 2023

No description provided.

@PatrickMassot PatrickMassot merged commit 873f494 into leanprover-community:master Feb 22, 2023
@PatrickMassot
Copy link
Member

Thanks!

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

Successfully merging this pull request may close these issues.

2 participants