1 files changed, 15 insertions, 0 deletions
diff --git a/configure b/configure
index 2b012c43..6255fc9a 100755
--- a/configure
+++ b/configure
@@ -135,6 +135,7 @@ lex_dbg_flags=${lex_dbg_flags-}
 txr_dbg_opts=${txr_dbg_opts---gc-debug}
 valgrind=${valgrind-}
 lit_align=${lit_align-}
+extra_debugging=${extra_debugging-}
 
 #
 # If --help was given (or --help=<nonempty> or help=<nonempty>) then
@@ -334,6 +335,11 @@ valgrind [$valgrind]
   Valgrind integration means that when the program is running under valgrind,
   it advises valgrind about stack memory locations accessed by the garbage
   collector, to suppress diagnostics about uninitialized accesses.
+
+extra_debugging [$extra_debugging]
+
+  Use --extra_debugging to configure some additional debugging features,
+  which incur a run-time penalty.
 !
   exit 1
 fi
@@ -922,6 +928,15 @@ else
 fi
 
 #
+# Extra debugging.
+#
+
+if [ -n "$extra_debugging" ] ; then
+  printf "Configuring extra debugging, as requested ...\n"
+  printf "#define EXTRA_DEBUGGING 1\n" >> config.h
+fi
+
+#
 # Clean up
 #