Closed anrddh closed 4 years ago
The current default (1G) is too low, especially when editing files in large projects like mathlib, so increase to the more reasonable 4G.
The current default (1G) is too low, especially when editing files in large projects like mathlib, so increase to the more reasonable 4G.