aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Clflags.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-08 16:28:00 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-08 16:28:00 +0200
commit96165dbec88ab4c951d99e64e51f5c55a1244137 (patch)
tree86110cecc1b97e39f2f8e5d58e228dd1dd10a1c5 /driver/Clflags.ml
parentda923568ad5085654b8db034310c4db50848e16e (diff)
downloadcompcert-kvx-96165dbec88ab4c951d99e64e51f5c55a1244137.tar.gz
compcert-kvx-96165dbec88ab4c951d99e64e51f5c55a1244137.zip
fixed a bug in support libraries; reload profiling info
Diffstat (limited to 'driver/Clflags.ml')
-rw-r--r--driver/Clflags.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 87c8d9c8..600c3371 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -84,4 +84,3 @@ let option_all_loads_nontrap = ref false
let option_inline_auto_threshold = ref 0
let option_profile_arcs = ref false
-