diff src/settings.sml @ 1633:deeeb036c8ed

Treat [naughtyDebug] as pure for optimization purposes
author Adam Chlipala <adam@chlipala.net>
date Mon, 05 Dec 2011 10:43:06 -0500
parents 438561303d02
children e374b6b8ab38
line wrap: on
line diff
--- a/src/settings.sml	Sun Dec 04 16:32:06 2011 -0500
+++ b/src/settings.sml	Mon Dec 05 10:43:06 2011 -0500
@@ -143,7 +143,6 @@
                         "onServerError",
                         "kc",
                         "debug",
-                        "naughtyDebug",
                         "rand",
                         "now",
                         "getHeader",