Fix duplicated list of profilers.

diff --git a/configure.py b/configure.py
index 92ad6d9811eb589bee66da142a01472b1fd1c608..16db7296e3cc8b6368515de6b4d599ec998f7e4b 100755 (executable)
--- a/configure.py
+++ b/configure.py
@@ -35,7 +35,7 @@ parser.add_option('--platform',
 parser.add_option('--debug', action='store_true',
                   help='enable debugging flags',)
 parser.add_option('--profile', metavar='TYPE',
-                  choices=['gmon', 'pprof'],
+                  choices=profilers,
                   help='enable profiling (' + '/'.join(profilers) + ')',)
 parser.add_option('--with-gtest', metavar='PATH',
                   help='use gtest built in directory PATH')