f67de7 Use the global identifier in the title of the pull_request page

Authored and Committed by Pierre-Yves Chibon 10 years ago
    Use the global identifier in the title of the pull_request page