diff --git a/bin/common_finput.cc b/bin/common_finput.cc index df0343dd1..14cd06b36 100644 --- a/bin/common_finput.cc +++ b/bin/common_finput.cc @@ -388,14 +388,14 @@ job_processor::run() return error; } -void check_no_formula() +void check_no_formula(const char* action) { if (!jobs.empty()) return; if (isatty(STDIN_FILENO)) - error(2, 0, "No formula to translate? Run '%s --help' for help.\n" + error(2, 0, "No formula to %s? Run '%s --help' for help.\n" "Use '%s -' to force reading formulas from the standard " - "input.", program_name, program_name); + "input.", action, program_name, program_name); jobs.emplace_back("-", job_type::LTL_FILENAME); } diff --git a/bin/common_finput.hh b/bin/common_finput.hh index 30b7f333c..491364d19 100644 --- a/bin/common_finput.hh +++ b/bin/common_finput.hh @@ -93,5 +93,5 @@ public: // Report and error message or add a default job depending on whether // the input is a tty. -void check_no_formula(); +void check_no_formula(const char* action = "translate"); void check_no_automaton(); diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc index 626211adc..61ffc3cd5 100644 --- a/bin/ltlgrind.cc +++ b/bin/ltlgrind.cc @@ -199,7 +199,7 @@ main(int argc, char* argv[]) mut_opts |= opt_all; - check_no_formula(); + check_no_formula("mutate"); mutate_processor processor; if (processor.run()) diff --git a/tests/core/ltlgrind.test b/tests/core/ltlgrind.test index f508c4826..bfceef88a 100755 --- a/tests/core/ltlgrind.test +++ b/tests/core/ltlgrind.test @@ -200,3 +200,11 @@ EOF ltlgrind -f 'a U b' -m 999999999999999999999999999 2>err && exit 1 grep 'too large' err + +# The following message appears only if run from a tty. +if (: > /dev/tty) >/dev/null 2>&1 ; then + ltlgrind err && exit 1 + grep 'No formula to mutate' err +fi + +: