be7090 Delete the temporary git repository once the pull-request has been merged or failed

Authored and Committed by Pierre-Yves Chibon 10 years ago
    Delete the temporary git repository once the pull-request has been merged or failed
    
        
file modified
+3 -0