You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
As mentioned in #730 we want to be able to mark something in the main branch as obsolete/deprecated, so it should print a warning that it will be removed soon.
We could do something like Semigroups with its obsolete.gi file, but we should think about how to do this in a nice way with synonyms.