Stream: Coq devs & plugin devs

Topic: ✔ Gitter archive


view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 17:58):

Hi folks, for the sake of our dev history preservation, I have managed to download the full archives of our old Gitter channel

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 17:58):

I understand we didn't have a copy, right? I had to play some tricks due to the current scripts being rate limited (cc @Théo Zimmermann )

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 17:59):

Now I have the raw data, I guess there should be something to render it, but let me know where I could upload the raw data, maybe in the wiki?

view this post on Zulip Théo Zimmermann (Mar 01 2022 at 18:00):

Note that all the Gitter messages were already available through Zulip (we migrated them when creating the Zulip org).

view this post on Zulip Théo Zimmermann (Mar 01 2022 at 18:00):

And you have unlimited search in the Zulip history.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 18:00):

Oh, thanks @Théo Zimmermann , I was under the impreesion that something had been done

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 18:01):

but had forgotten, so indeed the raw data is not needed

view this post on Zulip Notification Bot (Mar 01 2022 at 18:09):

Emilio Jesús Gallego Arias has marked this topic as resolved.


Last updated: Feb 05 2023 at 22:03 UTC