Add documentation of the --dev option on the init command

Change-Id: I6ee9c94991539d0b29e223830055d2286d49235f
diff --git a/Documentation/pgm-init.txt b/Documentation/pgm-init.txt
index 39cd70d..6aa3a74 100644
--- a/Documentation/pgm-init.txt
+++ b/Documentation/pgm-init.txt
@@ -11,6 +11,7 @@
 	[--no-auto-start]
 	[--list-plugins]
 	[--install-plugin=<PLUGIN_NAME>]
+        [--dev]
 --
 
 == DESCRIPTION
@@ -51,6 +52,10 @@
 	This option may be supplied more than once to install multiple
 	plugins.
 
+--dev::
+	Install in developer mode. Default configuration settings are
+	chosen to run the Gerrit server as a developer.
+
 == CONTEXT
 This command can only be run on a server which has direct
 connectivity to the metadata database, and local access to the