[gnome-user-docs] Consistently use <key> for characters in filenames

[Michael Hill <mdhill src gnome org>]

commit 96b041ba320422ead71393c60a3cfae6ccb4be9e
Author: Sebastian Rasmussen <sebras hotmail com>
Date:   Sun Sep 7 01:23:17 2014 +0200

    Consistently use <key> for characters in filenames
    
    Previously there were several occurrances in files-lost.page,
    files-rename.page, files-select.page and files-tilde.page that
    incorrectly used <file> or quotation marks to denote single
    characters in filenames.
    
    Fixes https://bugzilla.gnome.org/show_bug.cgi?id=736212

 gnome-help/C/files-lost.page   |    2 +-
 gnome-help/C/files-rename.page |    9 +++++----
 gnome-help/C/files-select.page |    4 ++--
 gnome-help/C/files-tilde.page  |    4 ++--
 4 files changed, 10 insertions(+), 9 deletions(-)
---
diff --git a/gnome-help/C/files-lost.page b/gnome-help/C/files-lost.page
index 73a8abe..37c8d20 100644
--- a/gnome-help/C/files-lost.page
+++ b/gnome-help/C/files-lost.page
@@ -47,7 +47,7 @@ follow these tips.</p>
   recover a deleted file.</p></item>
 
   <item><p>You might have renamed the file in a way that made the file hidden.
-  Files that start with a <file>.</file> or end with a <file>~</file> are hidden
+  Files that start with a <key>.</key> or end with a <key>~</key> are hidden
   in the file manager. Click the
   <media its:translate="no" type="image" src="figures/go-down.png"><span 
its:translate="yes">down</span></media> button in the file
   manager toolbar and pick <gui>Show Hidden Files</gui> to display them. See
diff --git a/gnome-help/C/files-rename.page b/gnome-help/C/files-rename.page
index 955b4e0..fc34f5f 100644
--- a/gnome-help/C/files-rename.page
+++ b/gnome-help/C/files-rename.page
@@ -42,10 +42,11 @@
   <link xref="nautilus-file-properties-basic">properties</link> window.</p>
 
   <p>When you rename a file, only the first part of the name of the file is
-  selected, not the file extension (the part after the "."). The extension
-  normally denotes what type of file it is (e.g. <file>file.pdf</file> is a PDF
-  document), and you usually do not want to change that. If you need to change
-  the extension as well, select the entire file name and change it.</p>
+  selected, not the file extension (the part after the <key>.</key>). The
+  extension normally denotes what type of file it is (e.g. <file>file.pdf</file>
+  is a PDF document), and you usually do not want to change that. If you need
+  to change the extension as well, select the entire file name and change
+  it.</p>
 
   <note style="tip">
     <p>If you renamed the wrong file, or named your file improperly, you can
diff --git a/gnome-help/C/files-select.page b/gnome-help/C/files-select.page
index 52e1b76..cb7a2ef 100644
--- a/gnome-help/C/files-select.page
+++ b/gnome-help/C/files-select.page
@@ -25,9 +25,9 @@
   two wild card characters available:</p>
 
   <list style="compact">
-    <item><p><file>*</file> matches any number of any characters, even
+    <item><p><key>*</key> matches any number of any characters, even
     no characters at all.</p></item>
-    <item><p><file>?</file> matches exactly one of any character.</p></item>
+    <item><p><key>?</key> matches exactly one of any character.</p></item>
   </list>
 
   <p>For example:</p>
diff --git a/gnome-help/C/files-tilde.page b/gnome-help/C/files-tilde.page
index a45ad1f..64e9129 100644
--- a/gnome-help/C/files-tilde.page
+++ b/gnome-help/C/files-tilde.page
@@ -21,9 +21,9 @@
     <include href="legal.xml" xmlns="http://www.w3.org/2001/XInclude"/>
   </info>
 
-<title>What is a file with a "~" at the end of its name?</title>
+<title>What is a file with a <key>~</key> at the end of its name?</title>
 
-  <p>Files with a "~" at the end of their names (for example,
+  <p>Files with a <key>~</key> at the end of their names (for example,
  <file>example.txt~</file>) are automatically created backup copies of documents
  edited in the <app>gedit</app> text editor or other applications. It is
  safe to delete them, but there's no harm to leave them on your computer.</p>