comparison make/jprt.properties @ 8657:63400866de15

pipeline: include PushNodesThroughPi according to % mx vm -G:Meter= | grep NodesPushed 3774 nodes (836 ReadNodes, 2938 IsNullNodes) are pushed.
author Bernhard Urban <bernhard.urban@jku.at>
date Fri, 05 Apr 2013 16:23:01 +0200
parents 3958f0acde31
children 3be6a41ad358
comparison
equal deleted inserted replaced
8656:369710426f74 8657:63400866de15