From ed7b8d69061082dfeae047268196c7c450ecbcd8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maximilian=20Ke=C3=9Fler?= Date: Thu, 17 Feb 2022 14:08:09 +0100 Subject: [PATCH] more legacy macros --- constants.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/constants.py b/constants.py index 8e1d9cd..81f0623 100644 --- a/constants.py +++ b/constants.py @@ -24,7 +24,8 @@ DEPRECATED = { r'\Tens': r'\tensor', r'\ann': r'\Ann', r'\Id': r'\id', - r'\cat': r'\mathcat' + r'\cat': r'\mathcat', + r'\ob': r'\Ob', } UNICODE = {