Make typenames a bit wider to support "existential type"

This commit is contained in:
Noah Lev 2023-06-23 10:12:27 -07:00
parent c4fca7202b
commit 12de5b7ff3

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: 6rem;
width: 7rem;
}
.popover {