Zulip Chat Archive
Stream: general
Topic: doc_gen
Patrick Massot (Feb 18 2020 at 23:03):
Rob, should we update https://github.com/leanprover-community/doc-gen/blob/master/print_docs.py#L56?
Rob Lewis (Feb 19 2020 at 11:20):
I guess it doesn't hurt, but right now that default is always replaced.
Last updated: Aug 03 2023 at 10:10 UTC