Skip to content
Snippets Groups Projects
Commit 73113843 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] fix legacy generator selection

parent d54cb480
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/Generator.ml
+ 1
− 1
View file @ 73113843
......@@ -64,7 +64,7 @@ let create
() : Wpo.generator =
let default f = function Some v -> v | None -> f () in
let dump = default Wp_parameters.Dump.get dump in
let legacy = default Wp_parameters.Dump.get legacy in
let legacy = default Wp_parameters.Legacy.get legacy in
let driver = default Driver.load_driver driver in
let setup = default user_setup setup in
if legacy then
......
src/plugins/wp/Generator.mli
+ 0
− 3
View file @ 73113843
......@@ -20,9 +20,6 @@
(* *)
(*****************************************t*********************************)
open Cil_types
open Wp_parameters
(* -------------------------------------------------------------------------- *)
(* --- WP Computer (main entry points) --- *)
(* -------------------------------------------------------------------------- *)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment