- Renamed '--monochrome' to '--plain', which is nicer and shorter.
This commit is contained in:
parent
3686a69869
commit
d21f292330
@ -90,7 +90,7 @@ switchesInit (int argc, char **argv)
|
|||||||
switches.reportStates = 0;
|
switches.reportStates = 0;
|
||||||
switches.extendNonReads = 0; // default off
|
switches.extendNonReads = 0; // default off
|
||||||
switches.extendTrivial = 0; // default off
|
switches.extendTrivial = 0; // default off
|
||||||
switches.monochrome = false; // default colors
|
switches.plain = false; // default colors
|
||||||
|
|
||||||
// Obsolete
|
// Obsolete
|
||||||
switches.latex = 0; // latex output?
|
switches.latex = 0; // latex output?
|
||||||
@ -908,15 +908,15 @@ switcher (const int process, int index, int commandline)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (detect (' ', "monochrome", 0))
|
if (detect (' ', "plain", 0))
|
||||||
{
|
{
|
||||||
if (!process)
|
if (!process)
|
||||||
{
|
{
|
||||||
helptext ("--monochrome", "disable color terminal output");
|
helptext ("--plain", "disable color terminal output");
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
switches.monochrome = true;
|
switches.plain = true;
|
||||||
return index;
|
return index;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -68,7 +68,7 @@ struct switchdata
|
|||||||
int reportStates; //!< Progress display switch. (traversed states)
|
int reportStates; //!< Progress display switch. (traversed states)
|
||||||
int extendNonReads; //!< Show further events in arachne xml output.
|
int extendNonReads; //!< Show further events in arachne xml output.
|
||||||
int extendTrivial; //!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension)
|
int extendTrivial; //!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension)
|
||||||
int monochrome; //!< Disable color output
|
int plain; //!< Disable color output
|
||||||
|
|
||||||
//! Latex output switch.
|
//! Latex output switch.
|
||||||
/**
|
/**
|
||||||
|
Loading…
Reference in New Issue
Block a user