+static void dump_comment (const char *comment)
+{
+ if (!strlen(comment)) return;
+ fprintf (tracing_file, "# %s\n", comment);
+}
+
+static void dump_comment_file (const char *filename)
+{
+ if (!strlen(filename)) return;
+ FILE *file = fopen (filename, "r");
+ if (!file){
+ THROWF (system_error, 1, "Comment file %s could not be opened for reading.", filename);
+ }
+ while (!feof(file)){
+ char c;
+ c = fgetc(file);
+ if (feof(file)) break;
+ fprintf (tracing_file, "# ");
+ while (c != '\n'){
+ fprintf (tracing_file, "%c", c);
+ c = fgetc(file);
+ if (feof(file)) break;
+ }
+ fprintf (tracing_file, "\n");
+ }
+ fclose(file);
+}
+
+