+void
+debug_vprintf(int indent, const char *format, va_list ap)
+{
+int save_errno = errno;
+
+if (!debug_file) return;
+
+/* Various things can be inserted at the start of a line. Don't use the
+tod_stamp() function for the timestamp, because that will overwrite the
+timestamp buffer, which may contain something useful. (This was a bug fix: the
++memory debugging with +timestamp did cause a problem.) */