FIX #2691: Manually reset the terminal to its initial settings; works around a bug...
authorJudah Jacobson <judah.jacobson@gmail.com>
Thu, 16 Oct 2008 02:48:38 +0000 (02:48 +0000)
committerJudah Jacobson <judah.jacobson@gmail.com>
Thu, 16 Oct 2008 02:48:38 +0000 (02:48 +0000)
commit758baa7c72043c44c91c0ba4f1fb7910cd7aa520
tree7a9cc7b357c525ff9d48fcb85bdc3811393319ca
parentec70c0a7512cd18ad08d23d69a8eea645fc8f2cf
FIX #2691: Manually reset the terminal to its initial settings; works around a bug in libedit.
compiler/ghci/InteractiveUI.hs