summaryrefslogtreecommitdiff
path: root/plugins/dp
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-04-19 16:52:57 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2011-04-19 16:52:57 +0200
commit7a24ebd7506f927a6493d065b8c9c297afd08db3 (patch)
tree3ee6d9c9aa5fc6cf6f793c1fb1a37c2307fd0287 /plugins/dp
parent4b1c150e26881501db9aa944df6406150fc0670d (diff)
parentaa33547c764a229e22d323ca213d46ea221b903e (diff)
Merge commit 'upstream/8.3.pl2+dfsg'
Diffstat (limited to 'plugins/dp')
-rw-r--r--plugins/dp/dp_why.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/dp/dp_why.ml b/plugins/dp/dp_why.ml
index 9a62f39d..199c3087 100644
--- a/plugins/dp/dp_why.ml
+++ b/plugins/dp/dp_why.ml
@@ -181,6 +181,5 @@ let print_query fmt (decls,concl) =
let output_file f q =
let c = open_out f in
let fmt = formatter_of_out_channel c in
- fprintf fmt "include \"real.why\"@.";
fprintf fmt "@[%a@]@." print_query q;
close_out c