From 335cc59f7dfc8295a99c223af4f8dc09bc2d05bb Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 19 Jul 2021 15:56:56 +0200
Subject: [PATCH] [dev] replace hard-coded usage of /dev/null in Sys.command
call
---
headers/hdrck.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/headers/hdrck.ml b/headers/hdrck.ml
index 8835c7d9890..3a173a6017d 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;
--
GitLab