Reduce typename width to 6.25rem

This makes "existential type" look slightly cramped (though still
readable), but it makes all other typenames look better. Existential
types are currently very rare, and we can always tweak this later if
necessary.
This commit is contained in:
Noah Lev 2023-06-23 12:02:55 -07:00
parent 12de5b7ff3
commit 5f433f33ed

View File

@ -894,7 +894,7 @@ so that we can apply CSS-filters to change the arrow color in themes */
display: inline-block;
color: var(--search-results-grey-color);
font-size: 0.875rem;
width: 7rem;
width: 6.25rem;
}
.popover {