michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(shell/lean): rename multi-threading option to -j

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-23 14:35:02 -07:00
parent 13fe28dd1c
commit 71afb83fcd
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/shell/lean.cpp
View file

@ -73,7 +73,7 @@ static void display_help(std::ostream & out) {
std::cout << " --quiet -q do not print verbose messages\n";
std::cout << " --interactive -i read blocks of commands from the input stream\n";
std::cout << " --hott use Homotopy Type Theory kernel and libraries\n";
std::cout << " --threads=num -r number of threads used to process lean files\n";
std::cout << " --threads=num -j number of threads used to process lean files\n";
std::cout << " --deps just print dependencies of a Lean input\n";
#if defined(LEAN_USE_BOOST)
std::cout << " --tstack=num -s thread stack size in Kb\n";
@ -107,7 +107,7 @@ static struct option g_long_options[] = {
{"interactive", no_argument, 0, 'i'},
{"quiet", no_argument, 0, 'q'},
{"hott", no_argument, 0, 'H'},
{"threads", required_argument, 0, 'r'},
{"threads", required_argument, 0, 'j'},
{"deps", no_argument, 0, 'D'},
#if defined(LEAN_USE_BOOST)
{"tstack", required_argument, 0, 's'},
@ -116,9 +116,9 @@ static struct option g_long_options[] = {
};
#if defined(LEAN_USE_BOOST)
static char const * g_opt_str = "DHiqlupgvhr:012c:012s:012t:012o:";
static char const * g_opt_str = "DHiqlupgvhj:012c:012s:012t:012o:";
#else
static char const * g_opt_str = "DHiqlupgvhr:012c:012t:012o:";
static char const * g_opt_str = "DHiqlupgvhj:012c:012t:012o:";
#endif
enum class lean_mode { Standard, HoTT };
@ -140,7 +140,7 @@ int main(int argc, char ** argv) {
if (c == -1)
break; // end of command line
switch (c) {
case 'r':
case 'j':
num_threads = atoi(optarg);
break;
case 'H':