Be a bit more flexible in terminal identification for do_bold
authorPepe Iborra <mnislaih@gmail.com>
Thu, 27 Sep 2007 14:15:49 +0000 (14:15 +0000)
committerPepe Iborra <mnislaih@gmail.com>
Thu, 27 Sep 2007 14:15:49 +0000 (14:15 +0000)
commit9efeaae7dd6d720b0f44b0a73ed4881d7eb41034
treedc26d216f445b71e7a8535ed3af76d59f25dffa4
parentbd3922fb7bac1d029d2c8bd311fb9d543120e8ca
Be a bit more flexible in terminal identification for do_bold

  In Os X for instance, by default we have TERM=xterm-color

MERGE TO STABLE
compiler/ghci/InteractiveUI.hs