diff options
-rwxr-xr-x | tools/configure | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tools/configure b/tools/configure index 2465c53a12..a50abb8d1d 100755 --- a/tools/configure +++ b/tools/configure | |||
@@ -303,10 +303,12 @@ whichsim () { | |||
303 | if [ -z "$simver" ]; then | 303 | if [ -z "$simver" ]; then |
304 | 304 | ||
305 | ################################################################## | 305 | ################################################################## |
306 | # Figure out win32/x11 GUI | 306 | # Figure out what simulator version |
307 | # | ||
308 | # x11 is deprecated so hide it from the question | ||
307 | # | 309 | # |
308 | echo "" | 310 | echo "" |
309 | echo "Build (W)in32 or (X)11 or (S)DL GUI version? (S)" | 311 | echo "Build (W)in32 or (S)DL version? (S)" |
310 | 312 | ||
311 | option=`input`; | 313 | option=`input`; |
312 | 314 | ||