| From: Shriram Krishnamurthi (sk at cs.brown.edu) Date: Mon Jul 26 17:14:11 EDT 2010 |
|
Yeah. I can make my window narrower, but the wider window helps for code. For now I'm just going to use two separate windows. Incidentally, I was surprised that the indenter got confused by Scribble. Should I be? Or perhaps the indenter doesn't claim to handle Scribble?
| Posted on the dev mailing list. |
|
![[logo]](/logo.png){kind=logo}