diff --git a/docs/users_guide/9.10.1-notes.rst b/docs/users_guide/9.10.1-notes.rst index 79de359b232904770230e15b98f16174aad21ae3..f2814d6370bc88ae7a6bc25cfe7e94f427b1ac5c 100644 --- a/docs/users_guide/9.10.1-notes.rst +++ b/docs/users_guide/9.10.1-notes.rst @@ -48,6 +48,9 @@ Compiler <https://github.com/agda/agda>`_, the size of the build results was reduced by about 10% when these info tables were omitted. +- Fixed a bug where compiling with both :ghc-flag:`-ddump-timings` and :ghc-flag:`-ddump-to-file` did not + suppress printing timings to the console. See :ghc-ticket:`20316`. + GHCi ~~~~