[PATCH 4/4] doc: convert git-request-pull synopsis and options to new style

["Jean-Noël Avila via GitGitGadget" <gitgitgadget@gmail.com>]

From: =?UTF-8?q?Jean-No=C3=ABl=20Avila?= <jn.avila@free.fr>

 * Replace [verse] with [synopsis] in the SYNOPSIS block
 * remove single-quote formatting from the command name
 * backtick-quote the flag
 * use _<placeholder>_ form for positional parameter terms

Signed-off-by: Jean-Noël Avila <jn.avila@free.fr>
---
 Documentation/git-request-pull.adoc | 38 +++++++++++++++++------------
 1 file changed, 23 insertions(+), 15 deletions(-)

diff --git a/Documentation/git-request-pull.adoc b/Documentation/git-request-pull.adoc
index 15dcbb6d91..8b6642b312 100644
--- a/Documentation/git-request-pull.adoc
+++ b/Documentation/git-request-pull.adoc
@@ -7,8 +7,8 @@ git-request-pull - Generates a summary of pending changes
 
 SYNOPSIS
 --------
-[verse]
-'git request-pull' [-p] <start> <URL> [<end>]
+[synopsis]
+git request-pull [-p] <start> <URL> [<end>]
 
 DESCRIPTION
 -----------
@@ -19,28 +19,28 @@ begins with the branch description, summarizes
 the changes, and indicates from where they can be pulled.
 
 The upstream project is expected to have the commit named by
-`<start>` and the output asks it to integrate the changes you made
-since that commit, up to the commit named by `<end>`, by visiting
-the repository named by `<URL>`.
+_<start>_ and the output asks it to integrate the changes you made
+since that commit, up to the commit named by _<end>_, by visiting
+the repository named by _<URL>_.
 
 
 OPTIONS
 -------
--p::
+`-p`::
 	Include patch text in the output.
 
-<start>::
+_<start>_::
 	Commit to start at.  This names a commit that is already in
 	the upstream history.
 
-<URL>::
+_<URL>_::
 	The repository URL to be pulled from.
 
-<end>::
-	Commit to end at (defaults to HEAD).  This names the commit
+_<end>_::
+	Commit to end at (defaults to `HEAD`).  This names the commit
 	at the tip of the history you are asking to be pulled.
 +
-When the repository named by `<URL>` has the commit at a tip of a
+When the repository named by _<URL>_ has the commit at a tip of a
 ref that is different from the ref you have locally, you can use the
 `<local>:<remote>` syntax, to have its local name, a colon `:`, and
 its remote name.
@@ -54,11 +54,15 @@ the `v1.0` release, and want it to be integrated into the project.
 First you push that change to your public repository for others to
 see:
 
-	git push https://git.ko.xz/project master
+-----
+git push https://git.ko.xz/project master
+-----
 
 Then, you run this command:
 
-	git request-pull v1.0 https://git.ko.xz/project master
+------
+git request-pull v1.0 https://git.ko.xz/project master
+------
 
 which will produce a request to the upstream, summarizing the
 changes between the `v1.0` release and your `master`, to pull it
@@ -67,11 +71,15 @@ from your public repository.
 If you pushed your change to a branch whose name is different from
 the one you have locally, e.g.
 
-	git push https://git.ko.xz/project master:for-linus
+-----
+git push https://git.ko.xz/project master:for-linus
+-----
 
 then you can ask that to be pulled with
 
-	git request-pull v1.0 https://git.ko.xz/project master:for-linus
+-----
+git request-pull v1.0 https://git.ko.xz/project master:for-linus
+-----
 
 
 GIT
-- 
gitgitgadget