Automatic pull of documentation from Wiki.

svn path=/trunk/; revision=5364

5 files changed, 10 insertions, 9 deletions

diff --git a/doc/doc.RPKI.CA.Configuration.irdbd b/doc/doc.RPKI.CA.Configuration.irdbd
index 9d00d0b6..41604ca1 100644
--- a/doc/doc.RPKI.CA.Configuration.irdbd
+++ b/doc/doc.RPKI.CA.Configuration.irdbd
@@ -1,8 +1,8 @@
 ****** [irdbd] section ******
 
 irdbd's default configuration file is the system rpki.conf file. Start irdbd
-with -c filename to choose a different configuration file. All options are in
-the section [irdbd].
+with "-c filename" to choose a different configuration file. All options are in
+the "[irdbd]" section.
 
 Since irdbd is part of the back-end system, it has direct access to the back-
 end's SQL database, and thus is able to pull its own BPKI configuration
diff --git a/doc/doc.RPKI.CA.Configuration.pubd b/doc/doc.RPKI.CA.Configuration.pubd
index 312e74c0..6dc7cb28 100644
--- a/doc/doc.RPKI.CA.Configuration.pubd
+++ b/doc/doc.RPKI.CA.Configuration.pubd
@@ -1,8 +1,8 @@
 ****** [pubd] section ******
 
 pubd's default configuration file is the system rpki.conf file. Start pubd with
--c filename to choose a different configuration file. All options are in the
-section [pubd]. BPKI certificates and keys may be either DER or PEM format.
+"-c filename" to choose a different configuration file. All options are in the
+"[pubd]" section. BPKI certificates and keys may be either DER or PEM format.
 
 ***** sql-database *****
 
diff --git a/doc/doc.RPKI.CA.Configuration.rootd b/doc/doc.RPKI.CA.Configuration.rootd
index ebb93d71..c3efba0f 100644
--- a/doc/doc.RPKI.CA.Configuration.rootd
+++ b/doc/doc.RPKI.CA.Configuration.rootd
@@ -19,8 +19,9 @@ Don't run rootd unless you're sure that you need to do so.
 Still think you need to run rootd? OK, but remember, you have been warned....
 
 rootd's default configuration file is the system rpki.conf file. Start rootd
-with -c filename to choose a different configuration file. All options are in
-the section [rootd]. Certificates and keys may be in either DER or PEM format.
+with "-c filename" to choose a different configuration file. All options are in
+the "[rootd]" section. Certificates and keys may be in either DER or PEM
+format.
 
 ***** bpki-ta *****
 
diff --git a/doc/doc.RPKI.CA.Configuration.rpkid b/doc/doc.RPKI.CA.Configuration.rpkid
index 5ce68be4..b1c9e38e 100644
--- a/doc/doc.RPKI.CA.Configuration.rpkid
+++ b/doc/doc.RPKI.CA.Configuration.rpkid
@@ -1,8 +1,8 @@
 ****** [rpkid] section ******
 
-rpkid's default config file is the system rpki.conf file. Start rpkid with -
-c filename to choose a different config file. All options are in the section
-[rpkid]. BPKI Certificates and keys may be in either DER or PEM format.
+rpkid's default config file is the system rpki.conf file. Start rpkid with "-
+c filename" to choose a different config file. All options are in the "[rpkid]"
+section. BPKI Certificates and keys may be in either DER or PEM format.
 
 ***** sql-database *****
 
diff --git a/doc/manual.pdf b/doc/manual.pdf
index d7bbff3d..8fe8789d 100644
--- a/doc/manual.pdf
+++ b/doc/manual.pdf