Stream: Coq devs & plugin devs

Topic: Github dev


view this post on Zulip Ali Caglayan (Sep 10 2021 at 09:21):

Did you know if you press . on a PR is opens up a web version of visual studio code? Doesn't look like you can actually run anything though, but thought it might be of interest.

view this post on Zulip Théo Zimmermann (Sep 10 2021 at 09:32):

Surprising! But it looks like it loads the file list indefinitely in my tests.

view this post on Zulip Théo Zimmermann (Sep 10 2021 at 09:34):

Or rather, it doesn't end up loading anything.


Last updated: Sep 09 2024 at 05:02 UTC