Generation number printed too

diff --git a/servers/is/dmp_kernel.c b/servers/is/dmp_kernel.c
index 0fc6669133e433573d70eb2d209464d5e9c206cd..7b08c892c98fd11ab44d0f3338e9fc1ffad5a94a 100644 (file)
--- a/servers/is/dmp_kernel.c
+++ b/servers/is/dmp_kernel.c
@@ -479,7 +479,7 @@ PUBLIC void proctab_dmp()
       return;
   }
 
-  printf("\n-nr-----endpoint--name--- -prior-quant- -user---sys----size-rts flags-\n");
+  printf("\n-nr-----gen---endpoint--name--- -prior-quant- -user---sys----size-rts flags-\n");
 
   for (rp = oldrp; rp < END_PROC_ADDR; rp++) {
        if (isemptyp(rp)) continue;
@@ -491,7 +491,7 @@ PUBLIC void proctab_dmp()
        if (proc_nr(rp) == IDLE)        printf("(%2d) ", proc_nr(rp));  
        else if (proc_nr(rp) < 0)       printf("[%2d] ", proc_nr(rp));
        else                            printf(" %2d  ", proc_nr(rp));
-       printf(" %10d ", rp->p_endpoint);
+       printf(" %5d %10d ", _ENDPOINT_G(rp->p_endpoint), rp->p_endpoint);
        printf(" %-8.8s %02u/%02u %02d/%02u %6lu%6lu %6uK %s",
               rp->p_name,
               rp->p_priority, rp->p_max_priority,