diff --git a/src/sinol_make/commands/run/__init__.py b/src/sinol_make/commands/run/__init__.py index 82e6ff59..cebe4415 100644 --- a/src/sinol_make/commands/run/__init__.py +++ b/src/sinol_make/commands/run/__init__.py @@ -1035,14 +1035,18 @@ def use_time(): if args.time_tool is None and self.config.get('sinol_undocumented_time_tool', '') != '': if self.config.get('sinol_undocumented_time_tool', '') == 'oiejq': timetool_path, timetool_name = use_oiejq() - else: + elif self.config.get('sinol_undocumented_time_tool', '') == 'time': timetool_path, timetool_name = use_time() + else: + util.exit_with_error('Invalid time tool specified in config.yml.') elif args.time_tool is None: timetool_path, timetool_name = use_default_timetool() elif args.time_tool == 'oiejq': timetool_path, timetool_name = use_oiejq() elif args.time_tool == 'time': timetool_path, timetool_name = use_time() + else: + util.exit_with_error('Invalid time tool specified.') return compilers, timetool_path, timetool_name def exit(self):