Fix duplicated list of profilers.
authorNicolas Despres <nicolas.despres@gmail.com>
Sat, 19 Nov 2011 14:48:30 +0000 (15:48 +0100)
committerNicolas Despres <nicolas.despres@gmail.com>
Sat, 19 Nov 2011 14:48:30 +0000 (15:48 +0100)
configure.py

index 92ad6d9811eb589bee66da142a01472b1fd1c608..16db7296e3cc8b6368515de6b4d599ec998f7e4b 100755 (executable)
@@ -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')