From 331569c9a8e7bbde41668a92dda5a174c47cc8af Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Thu, 29 Jul 2004 13:15:29 +0000
Subject: [PATCH] - Added '--echo' to stdout the commandline. Useful for
 reporting.

---
 src/main.c   | 15 ++++++++++-----
 src/output.c |  2 +-
 src/system.c |  1 -
 3 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/main.c b/src/main.c
index 6e9f6ef..dccf7f6 100644
--- a/src/main.c
+++ b/src/main.c
@@ -114,6 +114,7 @@ main (int argc, char **argv)
   struct arg_lit *switch_disable_noclaims_reductions = arg_lit0 (NULL, "no-noclaims-red", "disable no more claims reductions");
   struct arg_lit *switch_disable_endgame_reductions = arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions");
   struct arg_lit *switch_summary = arg_lit0 ("S", "summary", "show summary on stdout instead of stderr");
+  struct arg_lit *switch_echo = arg_lit0 ("E", "echo", "echo command line to stdout");
 #ifdef DEBUG
   struct arg_int *switch_por_parameter = arg_int0 (NULL, "pp", NULL, "POR parameter");
   struct arg_lit *switch_debug_indent = arg_lit0 ("I", "debug-indent",
@@ -133,6 +134,7 @@ main (int argc, char **argv)
     switch_scenario,
     switch_latex_output,
     switch_summary,
+    switch_echo,
     switch_progress_bar, 
 
     switch_traversal_method, 
@@ -298,11 +300,14 @@ main (int argc, char **argv)
   /* transfer command line */
   sys->argc = argc;
   sys->argv = argv;
-#ifdef DEBUG
-  /* print command line */
-  commandlinePrint (stderr, sys);
-  fprintf (stderr, "\n");
-#endif
+
+  if (switch_echo->count > 0)
+    {
+      /* print command line */
+      fprintf (stdout, "command\t");
+      commandlinePrint (stdout, sys);
+      fprintf (stdout, "\n");
+    }
 
   /* handle switches */
 
diff --git a/src/output.c b/src/output.c
index dd3dd94..cbc8743 100644
--- a/src/output.c
+++ b/src/output.c
@@ -505,7 +505,7 @@ void graphInit (const System sys)
   printf ("digraph Statespace {\n");
 
   /* label */
-  printf ("\tcomment = \"");
+  printf ("\tcomment = \"$");
   commandlinePrint (stdout, sys);
   printf ("\";\n");
 
diff --git a/src/system.c b/src/system.c
index 953d8f9..6fd4578 100644
--- a/src/system.c
+++ b/src/system.c
@@ -865,7 +865,6 @@ commandlinePrint (FILE *stream, const System sys)
   /* print command line */
   int i;
 
-  fprintf (stream, "$");
   for (i = 0; i < sys->argc; i++)
     fprintf (stream, " %s", sys->argv[i]);
 }