fix archive extension

07a103ce · Ivan D'halluin · 47fbf7c4 · 07a103ce
Commit 07a103ce authored Dec 17, 2015 by Ivan D'halluin
--- a/optim_to_hdoc/optim_to_hdoc.ant
+++ b/optim_to_hdoc/optim_to_hdoc.ant
@@ -72,7 +72,7 @@
    <sequential>
      <local name="folder_name"/>
      <basename property="folder_name" file="@{folder}"/>
-      <zip destfile="${out}/${folder_name}.zip" basedir="@{folder}" ></zip>
+      <zip destfile="${out}/${folder_name}.hdoc" basedir="@{folder}" ></zip>
    </sequential>
  </for>