Re: BUG: zsh-3.1.5-pws-24: time is dead

[Sven Wischnowsky <wischnow@informatik.hu-berlin.de>]

mason@primenet.com.au wrote:

> Heyla,
> % zsh -f
> % time =echo foobar
> foobar
> % =time =echo foobar
> foobar
>         0.01 real         0.00 user         0.01 sys
> % which -a time
> time: shell reserved word
> /usr/bin/time
> %

It may well be that it was me who broke this.

This patch seems to work, but since I don't know why it worked before, 
I'm not really happy with it.

Bye
 Sven

diff -u os/jobs.c Src/jobs.c
--- os/jobs.c	Wed Jun 30 11:56:49 1999
+++ Src/jobs.c	Thu Jul  1 08:31:58 1999
@@ -494,9 +494,14 @@
     int conted = 0, lineleng = columns, skip = 0, doputnl = 0;
     FILE *fout = (synch == 2) ? stdout : shout;
 
-    if (jn->stat & STAT_NOPRINT)
+    if (jn->stat & STAT_NOPRINT) {
+	if ((jn->stat & (STAT_TIMED | STAT_DONE)) == (STAT_TIMED | STAT_DONE) &&
+	    should_report_time(jn)) {
+	    jn->stat &= ~STAT_TIMED;
+	    dumptime(jn);
+	}
 	return;
-
+    }
     if (lng < 0) {
 	conted = 1;
 	lng = 0;

--
Sven Wischnowsky                         wischnow@informatik.hu-berlin.de