diff options
Diffstat (limited to 'distro-configs/Jenkins/Linux_ubsan_master.conf')
| -rw-r--r-- | distro-configs/Jenkins/Linux_ubsan_master.conf | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/distro-configs/Jenkins/Linux_ubsan_master.conf b/distro-configs/Jenkins/Linux_ubsan_master.conf new file mode 100644 index 000000000..8e7f80550 --- /dev/null +++ b/distro-configs/Jenkins/Linux_ubsan_master.conf @@ -0,0 +1,29 @@ +--disable-ld +--disable-ooenv +--enable-avahi +--enable-dbgutil +--enable-dbus +--enable-eot +--enable-epm +--enable-evolution2 +--enable-ext-ct2n +--enable-ext-languagetool +--with-system-mariadb +--enable-ext-nlpsolver +--enable-ext-numbertext +--enable-ext-wiki-publisher +--enable-gstreamer-1-0 +--enable-python=fully-internal +--enable-release-build +--enable-vlc +--enable-werror +--with-help +--with-lang=de en-US fi hu +--with-myspell-dicts +--without-system-libpng +--without-system-libxml +--without-system-zlib +--with-system-cairo +--disable-compiler-plugins +--disable-gtk3 +--with-jdk-home=/etc/alternatives/java_sdk_11 |