| From: Chongkai Zhu (czhu at cs.utah.edu) Date: Mon Feb 15 16:20:51 EST 2010 |
|
Whatever file attach we will use, I just want to remove the ".scrbl" extension and make all scribble file have the same extension as other files. The idea is to use the first #lang line to decide what "module" language it is, right? Chongkai
| Posted on the dev mailing list. |
|
![[logo]](/logo.png){kind=logo}