Distinguish between CONFIG_DEBUG and CONFIG_DEBUG_TOOLS in config files,

but in the Makefiles yet, because I want to keep the old config system
for a short while.

diff --git a/build/sherlock.cfg b/build/sherlock.cfg
index b8d5902629f52029d322907144458305dc5d5d93..8ecaac4ba42966982e45abad1ba6c0be12cd2cb2 100644 (file)
--- a/build/sherlock.cfg
+++ b/build/sherlock.cfg
@@ -7,6 +7,9 @@ Set("SHERLOCK_VERSION" => "3.5");
 # Installation directory for `make install'
 Set("INSTALL_DIR" => "~/run-3.5");
 
+# Compile everything with debug information and ASSERT's
+UnSet("CONFIG_DEBUG");
+
 ### Standard modules available in all releases of Sherlock ###
 
 # Gatherer (the gatherer library and some utilities) [FIXME: decide automatically?]
@@ -72,7 +75,7 @@ Set("CONFIG_MAX_CONTEXTS" => 256);
 Set("CONFIG_32BIT_REFERENCES");
 
 # Debugging tools
-UnSet("CONFIG_DEBUG");
+UnSet("CONFIG_DEBUG_TOOLS");
 
 # Search server: Enable EXPLAIN command (slows searching down slightly)
 Set("CONFIG_EXPLAIN");