diff --git a/headers/hdrck.ml b/headers/hdrck.ml index 8835c7d989036f15694ed917e08df44ebb3b3ebb..3a173a6017d284ee3fdff301ea2f54d6721c54e4 100755 --- a/headers/hdrck.ml +++ b/headers/hdrck.ml @@ -538,7 +538,7 @@ and print_usage () = let _ = (* Test if headache is in the path *) - if Sys.command "headache -e >/dev/null 2>/dev/null" <> 0 then + if Sys.command "headache -e" <> 0 then (Format.eprintf "error: 'headache' command not in PATH or incompatible \ version (option -e unsupported)@."; exit 6); Arg.parse (Arg.align (sort argspec)) (fun s -> spec_files := s::!spec_files) umsg;