diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-08-23 20:25:46 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-08-23 20:25:46 +0200 |
| commit | 25508b2953ff8d0941c257ee1cb887278cfebd79 (patch) | |
| tree | 15230cfa6234e357c5072c4c9d0a6367a5a72efa /driver/Driver.ml | |
| parent | 20b311376d93fd68d51a66ac4c158c000333ae18 (diff) | |
| download | compcert-25508b2953ff8d0941c257ee1cb887278cfebd79.tar.gz compcert-25508b2953ff8d0941c257ee1cb887278cfebd79.zip | |
Added error message when no input file is specified.
Diffstat (limited to 'driver/Driver.ml')
| -rw-r--r-- | driver/Driver.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 37e3b44c..e787b935 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -683,6 +683,11 @@ let _ = eprintf "Ambiguous '-o' option (multiple source files)\n"; exit 2 end; + if !num_source_files = 0 then + begin + eprintf "ccomp: error: no input file\n"; + exit 2 + end; let linker_args = time "Total compilation time" perform_actions () in if (not nolink) && linker_args <> [] then begin linker (output_filename_default "a.out") linker_args |