Skip to content

Install TLAUC in gitpod & codespaces - #104

Merged
ahelwer merged 1 commit into
tlaplus:masterfrom
ahelwer:devcontainer-tlauc
Jan 18, 2024
Merged

Install TLAUC in gitpod & codespaces#104
ahelwer merged 1 commit into
tlaplus:masterfrom
ahelwer:devcontainer-tlauc

Conversation

@ahelwer

@ahelwer ahelwer commented Jan 14, 2024

Copy link
Copy Markdown
Collaborator

Closes #99

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
@ahelwer

ahelwer commented Jan 14, 2024

Copy link
Copy Markdown
Collaborator Author

@lemmy should all this stuff installed in .devcontainer/install.sh be available in https://gitpod.io/#https://github.com/tlaplus/examples/? I started one and can't see it.

Edit: ah, I see that's set up from the .gitpod.Dockerfile instead. Also why are all the paths repeated in the .devcontainer/install.sh file?

@lemmy

lemmy commented Jan 14, 2024

Copy link
Copy Markdown
Member

Yes, Gitpod used to work. Maybe bitrot?! Have you confirmed that things work on codes paces?

@ahelwer
ahelwer merged commit a46ca79 into tlaplus:master Jan 18, 2024
@ahelwer
ahelwer deleted the devcontainer-tlauc branch January 18, 2024 14:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

Install TLA+ unicode converter into gitpod and codespaces

2 participants