diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-19 18:07:08 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-19 18:07:08 +0200 |
commit | 50ed2827867238a98f2036f799d4d6f354a2581c (patch) | |
tree | 5efa4083cd9de0faa04430d48f56c9e186a8e5e7 /driver/Clflags.ml | |
parent | 6885cf5c6cf05886a7dd09a3d4bfad079b628376 (diff) | |
download | compcert-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.ml | 1 |
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 |