Stream: Coq devs & plugin devs

Topic: clone with --single-branch in CI?

view this post on Zulip Gaëtan Gilbert (Sep 25 2020 at 12:52):

Should we clone with --single-branch in CI? The release branches would need to revert to use untagged commit hashes.

view this post on Zulip Théo Zimmermann (Sep 25 2020 at 18:35):

What do you call untagged commit hashes? Commit hashes not linked to a branch?

view this post on Zulip Gaëtan Gilbert (Sep 25 2020 at 19:15):

y

Last updated: Oct 16 2021 at 01:03 UTC