Implement git remote rename

diff --git a/Makefile b/Makefile
index 40309e1537aef1475992de110b6c37144a94ad67..220de39914c4df3abf394ad052ebb1fd6f62d3f7 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1405,6 +1405,9 @@ endif
 install-doc:
        $(MAKE) -C Documentation install
 
+install-man:
+       $(MAKE) -C Documentation install-man
+
 install-html:
        $(MAKE) -C Documentation install-html
 
@@ -1414,6 +1417,9 @@ install-info:
 quick-install-doc:
        $(MAKE) -C Documentation quick-install
 
+quick-install-man:
+       $(MAKE) -C Documentation quick-install-man
+
 quick-install-html:
        $(MAKE) -C Documentation quick-install-html