[7643] HTML.pm put manual name after page name in title

[gavinsmith0123]

Revision: 7643
          http://svn.sv.gnu.org/viewvc/?view=rev&root=texinfo&revision=7643
Author:   gavin
Date:     2017-01-21 12:29:48 -0500 (Sat, 21 Jan 2017)
Log Message:
-----------
HTML.pm put manual name after page name in title

Modified Paths:
--------------
    trunk/ChangeLog
    trunk/tp/Texinfo/Convert/HTML.pm

Modified: trunk/ChangeLog
===================================================================
--- trunk/ChangeLog     2017-01-21 17:20:40 UTC (rev 7642)
+++ trunk/ChangeLog     2017-01-21 17:29:48 UTC (rev 7643)
@@ -1,5 +1,15 @@
 2017-01-21  Gavin Smith  <address@hidden>
 
+       * tp/Texinfo/Convert/HTML.pm (_file_header_information):
+       Place name of manual in parentheses after the name of the page, 
+       instead of before it.  This is so that if several pages from a 
+       single manual are displayed in separate browser tabs, the user
+       will be able to distinguish them if only part of each page title 
+       is shown in each tab.
+       Suggestion from Bryan Ferris <address@hidden>.
+
+2017-01-21  Gavin Smith  <address@hidden>
+
        * info/nodes.c (build_tags_and_nodes): Check that a buffer 
        offset isn't 0 before subtracting 1 from it.  This is to avoid 
        reading outside allocated memory for malformed input.  (Report 

Modified: trunk/tp/Texinfo/Convert/HTML.pm
===================================================================
--- trunk/tp/Texinfo/Convert/HTML.pm    2017-01-21 17:20:40 UTC (rev 7642)
+++ trunk/tp/Texinfo/Convert/HTML.pm    2017-01-21 17:29:48 UTC (rev 7643)
@@ -6202,7 +6202,7 @@
         and $command_string ne $self->{'title_string'}) {
       print STDERR "DO <title>\n"
         if ($self->get_conf('DEBUG'));
-      my $title_tree = $self->gdt('{title}: {element_text}', 
+      my $title_tree = $self->gdt('{element_text} ({title})', 
                    { 'title' => $self->{'title_tree'}, 
                    'element_text' => $self->command_text($command, 'tree')});
       $title = $self->convert_tree_new_formatting_context(