Closed vvolhejn closed 6 years ago
Merging as the changes are hopefully non-controversial. CI time is increased (~2:30) because of the fonts package, but I wouldn't worry about that right now
Merging as the changes are hopefully non-controversial. CI time is increased (~2:30) because of the fonts package, but I wouldn't worry about that right now