[wp/gui] flags -w -6-9-50

999734e6 · Patrick Baudin · a4b62504 · 999734e6
Commit 999734e6 authored 3 years ago by Patrick Baudin
--- a/src/plugins/wp/gui/dune
+++ b/src/plugins/wp/gui/dune
@@ -2,6 +2,6 @@
  (name wp_gui)
  (public_name frama-c-wp.gui)
  (optional)
-  (flags -open Frama_c_kernel -open Frama_c_gui -open Wp :standard)
+  (flags -open Frama_c_kernel -open Frama_c_gui -open Wp :standard -w -6-9-50)
  (libraries frama-c-wp.core frama-c.kernel frama-c.gui why3 qed lablgtk2)
 )