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

fix(frontends/lean): do not display Ctrl-D message on Windows

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-04 11:39:30 -08:00
parent d949dfd46d
commit 7b4ea75dee
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/parser.cpp
View file

@ -1604,8 +1604,10 @@ class parser::imp {
<< " Show Environment show objects in the environment, if [Num] provided, then show only the last [Num] objects" << endl
<< " Show Environment [num] show the last num objects in the environment" << endl
<< " Variable [id] : [type] declare/postulate an element of the given type" << endl
<< " Universe [id] [level] declare a new universe variable that is >= the given level" << endl
<< "Type Ctrl-D to exit" << endl;
<< " Universe [id] [level] declare a new universe variable that is >= the given level" << endl;
#if !defined(LEAN_WINDOWS)
regular(m_frontend) << "Type Ctrl-D to exit" << endl;
#endif
}
}