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