[tor-commits] [metrics-base/master] Add release version to headline and in case of 'dev' versions also the git revision.

[karsten at torproject.org]

commit e130139e1a551bcf3e6437a85799590600f4b096
Author: iwakeh <iwakeh at torproject.org>
Date:   Tue Feb 14 16:21:33 2017 +0000

    Add release version to headline and in case of 'dev' versions also the git revision.
    Implements 21614.
---
 java/base.xml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/java/base.xml b/java/base.xml
index 0cafa32..951dae5 100644
--- a/java/base.xml
+++ b/java/base.xml
@@ -151,16 +151,21 @@
     </javac>
   </target>
 
-  <target name="docs">
+  <target name="docs" depends="gitrev" >
     <tstamp>
       <format property="copyyear"
               pattern="yyyy"
               timezone="UTC" />
     </tstamp>
+    <condition property="headline"
+               value="${implementation-title} ${release.version}.${git.revision} API Documentation"
+               else="${implementation-title} ${release.version} API Documentation" >
+      <contains string="${release.version}" substring="-dev" />
+    </condition>
     <javadoc destdir="${docs}"
              stylesheetfile="${javadocstyle}"
              footer="&copy; ${copyyear} The Tor Project"
-             doctitle="${javadoc-title}"
+             doctitle="${headline}"
              overview="${basedir}/${resources}/overview.html"
              use="true"
              windowtitle="${javadoc-title}">