on master help sign in
Make IDE mode default to 70 character terminals
771ae4aDavid Raymond Christiansen
src/Idris/Output.hs+1−1
@@ -61,7 +61,7 @@ iRender d = do w <- getWidth
61 if n < 1
61 if n < 1
62 then renderPretty 1.0 1000000000 d
62 then renderPretty 1.0 1000000000 d
63 else renderPretty 0.8 n d
63 else renderPretty 0.8 n d
64− AutomaticWidth | ideMode -> return $ renderPretty 1.0 1000000000 d
64+ AutomaticWidth | ideMode -> return $ renderPretty 1.0 80 d
65 | otherwise -> do width <- runIO getScreenWidth
65 | otherwise -> do width <- runIO getScreenWidth
66 return $ renderPretty 0.8 width d
66 return $ renderPretty 0.8 width d
67
67