Revisions to post number filtering. #491

- "Post ID" -> "Post number" in user-facing interface.
- Improve example.

src/Filtering/Filter.coffee

@@ -156,7 +156,7 @@ Filter =
         subEntries: []
 
       for type in [
-        ['Post ID',          'postID']
+        ['Post number',      'postID']
         ['Name',             'name']
         ['Unique ID',        'uniqueID']
         ['Tripcode',         'tripcode']

src/General/Config.coffee

@@ -639,8 +639,8 @@ Config =
 
   filter:
     postID: """
-      # Highlight dubs:
-      #/(\\d)\\1$/;highlight
+      # Highlight dubs on [s4s]:
+      #/(\\d)\\1$/;highlight;top:no;boards:s4s
     """
 
     name: """

src/General/html/Settings/Filter-select.html

@@ -1,6 +1,6 @@
 <select name="filter">
   <option value="guide">Guide</option>
-  <option value="postID">Post ID</option>
+  <option value="postID">Post number</option>
   <option value="name">Name</option>
   <option value="uniqueID">Unique ID</option>
   <option value="tripcode">Tripcode</option>