aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-01-25 17:50:58 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-01-25 17:50:58 +0100
commitfb3ca7666c734010eb038851830fbb4e41b5fcb0 (patch)
treef22b8ff88c6043c4d3552323fcb8ac992bf00821 /driver/Driver.ml
parent89bd87cab8e6216b1f87389f93424468710e5f21 (diff)
downloadcompcert-fb3ca7666c734010eb038851830fbb4e41b5fcb0.tar.gz
compcert-fb3ca7666c734010eb038851830fbb4e41b5fcb0.zip
Allow .sx files for preprocessed assembler files.
GCC treats files with .sx extension in the same way as it treats files with .S suffix.
Diffstat (limited to 'driver/Driver.ml')
-rwxr-xr-xdriver/Driver.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index d154c95b..411fd85d 100755
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -271,6 +271,7 @@ Recognized source files:
.i or .p C source file that should not be preprocessed
.cm Cminor source file
.s Assembly file
+ .sx Assembly file that must be preprocessed
.S Assembly file that must be preprocessed
.o Object file
.a Library file
@@ -503,6 +504,8 @@ let cmdline_actions =
push_action process_s_file s; incr num_source_files; incr num_input_files);
Suffix ".S", Self (fun s ->
push_action process_S_file s; incr num_source_files; incr num_input_files);
+ Suffix ".sx", Self (fun s ->
+ push_action process_S_file s; incr num_source_files; incr num_input_files);
Suffix ".o", Self (fun s -> push_linker_arg s; incr num_input_files);
Suffix ".a", Self (fun s -> push_linker_arg s; incr num_input_files);
(* GCC compatibility: .o.ext files and .so files are also object files *)