diff options
| -rw-r--r-- | push/build.xml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/push/build.xml b/push/build.xml index 9a45b86cfe..958bd5bf8f 100644 --- a/push/build.xml +++ b/push/build.xml @@ -26,7 +26,9 @@ <union id="jar.includes"> <fileset dir="${result.dir}/js"> <include name="VAADIN/vaadinPush.js" /> + <include name="VAADIN/vaadinPush.js.gz" /> <include name="VAADIN/vaadinPush.debug.js" /> + <include name="VAADIN/vaadinPush.debug.js.gz" /> </fileset> </union> @@ -77,6 +79,10 @@ <arg file="${vaadinPush.js}" /> <arg file="${vaadinPush.debug.js}" /> </java> + + <!-- Gzipped versions --> + <gzip src="${vaadinPush.js}" destfile="${vaadinPush.js}.gz" /> + <gzip src="${vaadinPush.debug.js}" destfile="${vaadinPush.debug.js}.gz" /> </target> <target name="jar" depends="vaadinPush.js"> |