diff options
Diffstat (limited to 'driver/Driver.ml')
| -rw-r--r-- | driver/Driver.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index bb9ac7c..44037b2 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -234,8 +234,6 @@ let linker exe_name files = (* Processing of a .c file *) -let option_interp = ref false - let process_c_file sourcename = if !option_E then begin preprocess sourcename (output_filename_default "-"); |