Add publish.xml for CI publishing

https://wiki.eclipse.org/Milestone_and_Release_Builds
https://bugs.eclipse.org/bugs/show_bug.cgi?id=545157

development/org.eclipse.libra.repository/publish.xml

diff --git a/development/org.eclipse.libra.repository/publish.xml b/development/org.eclipse.libra.repository/publish.xml
new file mode 100644
index 0000000..f7efd3d
--- /dev/null
+++ b/development/org.eclipse.libra.repository/publish.xml
@@ -0,0 +1,133 @@
+<!--
+  Copyright (c) 2019 Kiel University and others.
+  This program and the accompanying materials are made available under the
+  terms of the Eclipse Public License 2.0 which is available at
+  http://www.eclipse.org/legal/epl-2.0.
+  
+  SPDX-License-Identifier: EPL-2.0
+
+  Assembles the distribution of the whole thing and publishes (fancy word for
+  "copies") it at a target directory. By using only the tasks publish and purge,
+  this script can also be used simply to delete directories or copy one directory
+  over to a target directory. Here's the available tasks:
+  
+  * publish - The most important task. If only this task is called, the update
+              site (whose location is specified by ${sourceDir}) is published
+              at ${targetDir}.
+  * zipIt   - Includes a zipped version of the update site in the published
+              version.
+  * docs    - Builds the documentation website and includes a zipped version
+              of it.
+  
+  * purge   - A utility task not normally called. Simply removes the target
+              directory.
+  
+  Mandatory properties:
+  
+  * targetDir - The directory to publish everything at. This thing is emptied
+                  before things get published, so be careful to lose everything.
+                  This property MUST be set.
+  
+  Important properties:
+  
+  * version   - The ELK version. This is used to assemble ZIP file names.
+                  Defaults to "nightly".
+  
+  Optional properties:
+  
+  * sourceDir - The source directory where the update site was built. Defaults
+                  to where Maven builds the thing and does not usually have to
+                  be set.
+  * hugoPath  - Path to the Hugo executable. If Hugo is on the path, this does
+                  not need to be set at all. If it is not, the full path needs
+                  to be supplied to this script. Only used to execute the docs
+                  task.
+-->
+<project name="Webtools Libra" basedir=".">
+
+    <!-- ================================================================= -->
+    <!-- P R O P E R T I E S                                               -->
+    <!-- ================================================================= -->
+
+    <!-- Important -->
+    <property name="version" value="nightly" />
+
+    <!-- Optional -->
+    <property name="sourceDir" value="target/repository/" />
+    <property name="hugo" value="hugo" />
+
+    <!-- Internal -->
+    <property name="updateSiteZipFileName" value="libra-${version}.zip" />
+    <property name="docsSiteZipFileName" value="libra-${version}-docs.zip" />
+
+
+    <!-- ================================================================= -->
+    <!-- P U B L I S H                                                     -->
+    <!-- ================================================================= -->
+    <target name="publish"
+            description="Publishes the content of a source directory in a target directory.">
+
+        <!-- Empty the target directory -->
+        <delete dir="${targetDir}" />
+
+        <!-- Recreate the target directory. It can happen that this task
+             fails seemingly at random. To be sure, we wrap it in a retry
+             task that repeats the mkdir call up to 10 times, with a pause
+             between each pair of attempts (the retrydelay is measured in
+             milliseconds). -->
+        <retry retrycount="10" retrydelay="1000">
+            <mkdir dir="${targetDir}" />
+        </retry>
+
+        <!-- Copy to target directory -->
+        <copy todir="${targetDir}">
+            <fileset dir="${sourceDir}" />
+        </copy>
+    </target>
+
+
+    <!-- ================================================================= -->
+    <!-- Z I P   I T                                                       -->
+    <!-- ================================================================= -->
+    <target name="zipIt"
+            description="Produces a zip file from the update site directory.">
+
+        <!-- Produce a zip archive of the update site -->
+        <zip destfile="${sourceDir}/${updateSiteZipFileName}"
+             basedir="${sourceDir}"
+             excludes="${docsSiteZipFileName}"
+        />
+    </target>
+
+
+    <!-- ================================================================= -->
+    <!-- D O C S                                                           -->
+    <!-- ================================================================= -->
+    <target name="docs"
+            description="Compiles and zips the documentation website.">
+
+        <!-- Empty the compilation directory -->
+        <delete dir="../../docs/public/" />
+
+        <!-- Invoke hugo to compile our documentation website -->
+        <exec executable="${hugo}"
+              dir="../../docs/"
+        />
+
+        <!-- Produce a zip archive of the documentation site -->
+        <zip destfile="${sourceDir}/${docsSiteZipFileName}"
+             basedir="../../docs/public/"
+        />
+    </target>
+
+
+    <!-- ================================================================= -->
+    <!-- P U R G E                                                         -->
+    <!-- ================================================================= -->
+    <target name="purge"
+            description="Purges the target directory by removing it.">
+
+        <delete dir="${targetDir}" />
+    </target>
+
+</project>