Zulip Chat Archive
Stream: condensed mathematics
Topic: thm69_bad
Adam Topaz (Sep 23 2021 at 17:57):
It seems that laurent_measures/thm69_bad.lean is making the CI unhappy. @Filippo A. E. Nuccio do you still need this file? Perhaps you can comment out the contents?
Filippo A. E. Nuccio (Sep 23 2021 at 17:57):
Sure! Give me one sec
Filippo A. E. Nuccio (Sep 23 2021 at 17:59):
Done, and pushed!
Adam Topaz (Sep 23 2021 at 17:59):
Thanks!
Last updated: Dec 20 2023 at 11:08 UTC