diff options
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r-- | driver/Driver.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 3aff4e0f..cee62501 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -257,12 +257,6 @@ let process_S_file sourcename = end; prefixname ^ ".o" -(* Interpretation of a .c file *) - -let execute_c_file sourcename = - let preproname = Filename.temp_file "compcert" ".i" in - preprocess sourcename preproname - (* Command-line parsing *) type action = |