From 4f20216677199792f784ed4aa43f6927bbafb417 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Mar 2014 17:14:26 -0800 Subject: [PATCH] fix documnetation to say milli-seconds. Issue 84 Signed-off-by: Nikolaj Bjorner --- src/shell/main.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/shell/main.cpp b/src/shell/main.cpp index e0fa4a1f2..f23bc470c 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -87,7 +87,7 @@ void display_usage() { std::cout << "\nResources:\n"; // timeout and memout are now available on Linux and OSX too. std::cout << " -T:timeout set the timeout (in seconds).\n"; - std::cout << " -t:timeout set the soft timeout (in seconds). It only kills the current query.\n"; + std::cout << " -t:timeout set the soft timeout (in milli seconds). It only kills the current query.\n"; std::cout << " -memory:Megabytes set a limit for virtual memory consumption.\n"; // std::cout << "\nOutput:\n";