aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Clflags.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-05-19 18:07:08 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-05-19 18:07:08 +0200
commit50ed2827867238a98f2036f799d4d6f354a2581c (patch)
tree5efa4083cd9de0faa04430d48f56c9e186a8e5e7 /driver/Clflags.ml
parent6885cf5c6cf05886a7dd09a3d4bfad079b628376 (diff)
downloadcompcert-50ed2827867238a98f2036f799d4d6f354a2581c.tar.gz
compcert-50ed2827867238a98f2036f799d4d6f354a2581c.zip
Added flag for the renaming of static functions.
Diffstat (limited to 'driver/Clflags.ml')
-rw-r--r--driver/Clflags.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 8899c2b0..d9c21a9c 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -59,3 +59,4 @@ let option_small_data =
then 8 else 0)
let option_small_const = ref (!option_small_data)
let option_timings = ref false
+let option_rename_static = ref false