Synopsis: "make -j2 dist" does not work (bad dependency?) State-Changed-From-To: closed->open State-Changed-By: pdmef State-Changed-When: Fri, 30 Mar 2007 11:42:29 +0200 State-Changed-Why: Reopened as it's not fixed. If it works then only by accident since makedoc is still compiled twice, i.e. there's a race of two compiler runs overwriting their results (if one is lucky, one linker writes makedoc after the other is completely done already; but I've seen them doing it concurrently).
**** Comment added by pdmef on Fri, 30 Mar 2007 11:42:29 +0200 ****
