From 7c1e148ffa0311df3df15456d95f8bf0b87ccbed Mon Sep 17 00:00:00 2001
From: "Gustavo J. A. M. Carneiro" <gjc@inescporto.pt>
Date: Thu, 21 Jun 2007 12:33:50 +0100
Subject: [PATCH] WAF: add a warning to the --high-precision-as-double option
 help text saying they it works in configure.

---
 src/simulator/wscript | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/simulator/wscript b/src/simulator/wscript
index 3f038d813..fec0412c0 100644
--- a/src/simulator/wscript
+++ b/src/simulator/wscript
@@ -7,7 +7,9 @@ import Params
 def set_options(opt):
     opt.add_option('--high-precision-as-double',
                    help=('Whether to use a double floating point'
-                         ' type for high precision time values'),
+                         ' type for high precision time values'
+                         ' WARNING: this option only has effect '
+                         'with the configure command.'),
                    action="store_true", default=False,
                    dest='high_precision_as_double')