+/* -----------------------------------------------------------------------------
+ * initStatsFile: write a line to the file containing the program name
+ * and the arguments it was invoked with.
+-------------------------------------------------------------------------- */
+
+static void initStatsFile (FILE *f)
+{
+ /* Write prog_argv and rts_argv into start of stats file */
+ int count;
+ for (count = 0; count < prog_argc; count++) {
+ stats_fprintf(f, "%s ", prog_argv[count]);
+ }
+ stats_fprintf(f, "+RTS ");
+ for (count = 0; count < rts_argc; count++)
+ stats_fprintf(f, "%s ", rts_argv[count]);
+ stats_fprintf(f, "\n");
+}