From 7b4ea75deea20aa33641b36a89a3394f422c4205 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Dec 2013 11:39:30 -0800 Subject: [PATCH] fix(frontends/lean): do not display Ctrl-D message on Windows Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 6205d93557..12e6f803e6 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -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 } }