[Bug libstdc++/53263] priority_queue is very slow if -D_GLIBCXX_DEBUG is used

[paolo.carlini at oracle dot com]

http://gcc.gnu.org/bugzilla/show_bug.cgi?id=53263

--- Comment #12 from Paolo Carlini <paolo.carlini at oracle dot com> 2012-05-12 
21:41:15 UTC ---
Francois, please double check that now you are ok, thanks.