From d1871d87dc80cb4687a3b944b48dc5482376a755 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 14 Oct 2012 18:29:34 +0200 Subject: [PATCH] * src/bin/ltlcheck.cc: Diagnose missing output format. --- src/bin/ltlcheck.cc | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/bin/ltlcheck.cc b/src/bin/ltlcheck.cc index 729cc2fae..c4396dd3d 100644 --- a/src/bin/ltlcheck.cc +++ b/src/bin/ltlcheck.cc @@ -491,6 +491,11 @@ namespace std::ostringstream command; format(command, translators[translator_num]); toclean.push_back(output.val()); + + if (output.format == printable_result_filename::None) + error(2, 0, "no output sequence used in %s", + translators[translator_num]); + std::string cmd = command.str(); std::cerr << "Running [" << l << translator_num << "]: " << cmd << std::endl;