#67 Continue optimizing space usage.

expln · Jun 8, 2023 · a87abd1 · a87abd1
1 parent e2e8e9c
commit a87abd1
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/src/metamath/ui/MM_cmp_user_stmt.res b/src/metamath/ui/MM_cmp_user_stmt.res
@@ -1143,7 +1143,12 @@ let make = React.memoCustomCompareProps( ({
                 longClickDelayMs
                 onShortClick = {_ => actToggleInfoExpanded()}
                 onLongClick=onTypEditRequested
-                style=ReactDOM.Style.make(~cursor="pointer", ~fontWeight="bold", ())
+                style=ReactDOM.Style.make(
+                    ~cursor="pointer", 
+                    ~fontWeight="bold", 
+                    ~padding="1px 5px",
+                    ()
+                )
                 title={
                     chgTypShortcutName ++ " to change statement type between P (provable), G (goal) and H (hypothesis). " 
                         ++ "Alt is sometimes labelled Opt. "