Merge branch 'improvement/JAL-1988+JAL-3416_Java8_macOS_APQHandlers_and_FlatLaF_optio...
[jalview.git] / utils / publishHelp.xml
1 <project name="Publish Help Webpages for Jalview" default="pubhtmlhelp">
2
3 <target name="pubhtmlhelp">
4   <property name="appletHelpDir" value="../build/distributions/help"/>
5         <!-- finally, publish the help files -->
6         <javac srcdir="." destdir="." includes="help2Website.java"/>
7         <java fork="true" dir="${helpBuildDir}" classpath="." classname="help2Website"/>
8         <delete dir="${appletHelpDir}"/>
9         <copy preservelastmodified="true" overwrite="true" 
10            todir="${appletHelpDir}">
11           <fileset dir="${helpBuildDir}">
12             <include name="*htm*"/>
13             <include name="icons/**.*"/>
14             <include name="html/**/*.*"/>
15             <exclude name="**/CVS"/>
16             <exclude name="CVS"/>
17           </fileset>
18         </copy>
19         <replace dir="${appletHelpDir}">
20         <include name="**/*.htm*"/>
21         <replacetoken><![CDATA[</body>]]></replacetoken>
22         <replacevalue><![CDATA[
23 <script type="text/javascript">
24     var gaJsHost = (("https:" == document.location.protocol) ?
25         "https://ssl." : "http://www.");
26     document.write(unescape("%3Cscript src=\'" + gaJsHost +
27         "google-analytics.com/ga.js\' type=\'text/javascript\'%3E%3C/script%3E"));
28 </script>
29 <script type="text/javascript">
30 try{
31     var pageTracker = _gat._getTracker("'UA-9060947-1'");
32     pageTracker._trackPageview();
33 } catch(err) {}
34 </script>
35 </body>
36 ]]></replacevalue>
37 </replace>
38 <echo file="${appletHelpDir}/help.html">
39 <![CDATA[<html><head>
40 <title>Jalview Documentation</title>
41 </head>
42 <frameset cols="300,*">
43 <frame src="helpTOC.html" name=tocframe scrolling=yes >
44 <frame src="html/index.html" name=bodyframe >
45 <noframes><body>
46 This page requires a browser that supports frames.
47 <script type="text/javascript">
48     var gaJsHost = (("https:" == document.location.protocol) ?
49         "https://ssl." : "http://www.");
50     document.write(unescape("%3Cscript src=\'" + gaJsHost +
51         "google-analytics.com/ga.js\' type=\'text/javascript\'%3E%3C/script%3E"));
52 </script>
53 <script type="text/javascript">
54 try{
55     var pageTracker = _gat._getTracker("'UA-9060947-1'");
56     pageTracker._trackPageview();
57 } catch(err) {}
58 </script></body>
59 <noframes></frameset>
60 </html>
61 ]]></echo>
62
63   </target>
64 </project>