Merge.

2 files changed, 5 insertions, 2 deletions

diff --git a/src/c/static.c b/src/c/static.c
index c8fd5bc7..7f63d393 100644
--- a/src/c/static.c
+++ b/src/c/static.c
@@ -37,7 +37,7 @@ int main(int argc, char *argv[]) {
   while (1) {
     fk = uw_begin(ctx, argv[1]);
 
-    if (fk == SUCCESS) {
+    if (fk == SUCCESS || fk == RETURN_INDIRECTLY) {
       uw_print(ctx, 1);
       puts("");
       return 0;
diff --git a/src/c/urweb.c b/src/c/urweb.c
index 3993448b..faef4d3a 100644
--- a/src/c/urweb.c
+++ b/src/c/urweb.c
@@ -4235,7 +4235,10 @@ void uw_check_deadline(uw_context ctx) {
 size_t uw_database_max = SIZE_MAX;
 
 uw_Basis_int uw_Basis_naughtyDebug(uw_context ctx, uw_Basis_string s) {
-  fprintf(stderr, "%s\n", s);
+  if (ctx->loggers->log_debug)
+    ctx->loggers->log_debug(ctx->loggers->logger_data, "%s\n", s);
+  else
+    fprintf(stderr, "%s\n", s);
   return 0;
 }