Re-add accidentally-deleted line
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 17 Oct 2016 08:23:50 +0000 (09:23 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 17 Oct 2016 08:23:50 +0000 (09:23 +0100)
commit3adaacde6b8ad6f41e1554598a9fd93d9e605bc2
tree792227034678c95cec26e7f9b8aef02d7f35e4d9
parentf43db14e2cae9cd181b283cdc7d7940903689bf6
Re-add accidentally-deleted line

This adds a line I deleted by mistake in

  commit db71d971379c74dd1d2b958c11dc6c9e718a3e61
  Author: Simon Peyton Jones <simonpj@microsoft.com>
  Date:   Fri Oct 14 17:40:51 2016 +0100

      Reduce trace output slightly

Sorry about that!
compiler/typecheck/TcSMonad.hs