Suppose I have the following syntax: HH:MM:SS. I want to make it as short as possible. For example, I want "00:00:30" To turn into "30". Similarly, I want "0:30:00" to turn into "30:00". How can I do this with shell commands?
- 10What output you would expect with 00:00:00.schrodingerscatcuriosity– schrodingerscatcuriosity2022-06-22 22:35:51 +00:00Commented Jun 22, 2022 at 22:35
Add a comment |
1 Answer
As I understand you need to remove the leading zeroes, so let's suppose you have a file like this
00:00:30 00:01:30 00:30:00 01:30:00 30:00:00 would become
30 1:30 30:00 1:30:00 30:00:00 If that's so, you just need to apply a sed command like this:
sed 's/^[0:]*//' file answered Jun 22, 2022 at 1:31
schrodingerscatcuriosity
12.8k5 gold badges38 silver badges64 bronze badges
- 11Consider adding
00:00:00to the example. I read "as much as possible" and my formal brain totally enjoys what happens to this exact string. :DKamil Maciorowski– Kamil Maciorowski2022-06-22 18:47:43 +00:00Commented Jun 22, 2022 at 18:47 - @KamilMaciorowski Good one :), I' d guess it would be 0... asked to OP.schrodingerscatcuriosity– schrodingerscatcuriosity2022-06-22 22:34:59 +00:00Commented Jun 22, 2022 at 22:34
- 3Why, though? You would save a tiny amount of storage space and guarantee that your result was non-standard…Robbie Goodwin– Robbie Goodwin2022-06-22 23:14:31 +00:00Commented Jun 22, 2022 at 23:14
- 7Non-sortable as well.reinierpost– reinierpost2022-06-23 08:35:47 +00:00Commented Jun 23, 2022 at 8:35
- 2If you want the "00:00:00" → "0" case to be handled too: ` sed -e 's/^[0:]*//' -e 's/^$/0/'` - this will cause an empty string to be turned back into a single zero. There're probably more ways to achieve this.BotOfWar– BotOfWar2022-06-23 15:21:09 +00:00Commented Jun 23, 2022 at 15:21