leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: Zulip meta

Topic: Editing titles of posts - `this title is deliberately long`


Eric Wieser (Jan 13 2021 at 15:44):

It seems to me that if you edit the title of a post, the length requirement of the edit is shorter than the original?

Eric Wieser (Jan 13 2021 at 15:46):

Ah, got it - when making a new post, zulip prevents you using too long a title.

When editing a post, zulip just truncates the title with ...s without warning


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll