Zulip Chat Archive

Stream: general

Topic: tutorials and gitpod

Johan Commelin (Dec 30 2021 at 15:19):

Can we make the tutorials project gitpod enabled? How hard would that be?

Patrick Massot (Dec 30 2021 at 15:20):

This is probably easy. It only takes someone knowing about gitpod.

Eric Wieser (Dec 30 2021 at 15:33):

You should be able to directly copy the gitpod file from lean-liquid

Johan Commelin (Dec 30 2021 at 15:50):

@Eric Wieser voila: https://github.com/leanprover-community/tutorials/pull/42

Last updated: Dec 20 2023 at 11:08 UTC