diff --git a/docs/users_guide/using-optimisation.rst b/docs/users_guide/using-optimisation.rst index adc888353261d86b455708f6786b3543ca28850e..b99c68a3202dbdf0c65c843b92d7f7ec2235b6b8 100644 --- a/docs/users_guide/using-optimisation.rst +++ b/docs/users_guide/using-optimisation.rst @@ -1851,6 +1851,8 @@ as such you shouldn't need to set any of them explicitly. A flag :default: 2 + :since: 9.12.1 + This flag defines the level of compression of interface files when writing to disk. The higher the flag, the more we deduplicate the interface file, at the cost of a higher compilation time. Deduplication (when applied to :ghc-flag:`--make` mode and :ghc-flag:`--interactive` mode) decreases the size of interface files as well as reducing