aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-01-25 10:03:11 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-01-25 10:03:11 +0100
commit4467453e0edca993c175690b7141d4916af3dc19 (patch)
tree15bd43200c36a5bc5d57c87a3e1220e378df07aa /driver/Driver.ml
parent507f000343636e1e300b1f3af71177726926292c (diff)
downloadcompcert-4467453e0edca993c175690b7141d4916af3dc19.tar.gz
compcert-4467453e0edca993c175690b7141d4916af3dc19.zip
Started implementing a printer for Clflags.
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 78d141c1..d827fd94 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -14,6 +14,7 @@ open Printf
open Commandline
open Camlcoq
open Clflags
+open Clflagsprinter
open Timing
(* Location of the compatibility library *)