From a452c75338892f449813d25d3a17f4fa580b6760 Mon Sep 17 00:00:00 2001 From: Joachim Ansorg Date: Mon, 31 Oct 2022 15:23:35 +0100 Subject: [PATCH] Added meaningful page for apparently broken content --- SC2023.md | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/SC2023.md b/SC2023.md index 8a375d8..71b5df6 100644 --- a/SC2023.md +++ b/SC2023.md @@ -1 +1,22 @@ -The shell may override 'time' as seen in man time(1). Use 'command time ..' for that one. \ No newline at end of file +## The shell may override `time` as seen in man time(1). Use `command time ..` for that one. + +### Problematic code: + +```sh +time -some some +``` + +### Correct code: + +```sh +command time -some some +``` + +### Rationale: + +`time` is a built-in command. +If you would like to use `time` from `$PATH`, you need to use `command` to execute it as a regular command. + +### Exceptions: + +None \ No newline at end of file