- if (strequal(rts_argv[arg]+2, "stderr")) /* use real stderr */
- f = stderr;
- else if (rts_argv[arg][2] != '\0') /* stats file specified */
- f = fopen(rts_argv[arg]+2,"w");
- else {
- char stats_filename[STATS_FILENAME_MAXLEN]; /* default <program>.<ext> */
- sprintf(stats_filename, FILENAME_FMT, argv[0]);
- f = fopen(stats_filename,"w");
- }
- if (f == NULL) {
- fprintf(stderr, "Can't open stats file %s\n", rts_argv[arg]+2);
+ if (strequal(rts_argv[arg]+2, "stderr")) { /* use debugBelch */
+ f = NULL; /* NULL means use debugBelch */