diff options
| -rwxr-xr-x | build/ide.xml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/build/ide.xml b/build/ide.xml index 4bd839365f..d468473392 100755 --- a/build/ide.xml +++ b/build/ide.xml @@ -181,7 +181,7 @@ <property name="js.output.dir" location="WebContent" /> <property name="push.js.dir" location="${basedir}/push/result/js" /> <copy todir="${js.output.dir}"> - <fileset dir="${push.js.dir}" includes="VAADIN/vaadinPush*"> + <fileset dir="${push.js.dir}" includes="VAADIN/vaadinPush*" excludes="**/*.gz"> </fileset> </copy> </target> |