Correct a bug which could replace "makeinfo" with "make -j1info"
This commit is contained in:
parent
e58cf15308
commit
9c5ea2fa6f
1 changed files with 10 additions and 7 deletions
|
@ -480,7 +480,10 @@ popd</xsl:text>
|
|||
contains(string(),'check'))">
|
||||
<xsl:text>#</xsl:text>
|
||||
<xsl:value-of select="substring-before(string(),'make ')"/>
|
||||
<xsl:text>make -k</xsl:text>
|
||||
<xsl:text>make </xsl:text>
|
||||
<xsl:if test="not(contains(string(),'-k'))">
|
||||
<xsl:text>-k </xsl:text>
|
||||
</xsl:if>
|
||||
<xsl:value-of select="substring-after(string(),'make ')"/>
|
||||
<xsl:text> || true
</xsl:text>
|
||||
</xsl:if>
|
||||
|
|
Loading…
Reference in a new issue