Make IDE mode default to 70 character terminals
commit771ae4ae5e330132be49a2a7d49fcdd302e43474
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateMon 16 Mar 2015, 19:29 (12 years ago)
parent3d87454
src/Idris/Output.hs+1−1
@@ -61,7 +61,7 @@ iRender d = do w <- getWidth
6161 if n < 1
6262 then renderPretty 1.0 1000000000 d
6363 else renderPretty 0.8 n d
64− AutomaticWidth | ideMode -> return $ renderPretty 1.0 1000000000 d
64+ AutomaticWidth | ideMode -> return $ renderPretty 1.0 80 d
6565 | otherwise -> do width <- runIO getScreenWidth
6666 return $ renderPretty 0.8 width d
6767