Re: [PATCH evolve-ext] debian: add line to clean-docs target to delete additional docs file

I was checking the in-flight patches and saw that we never acknowledge the reception of those patches. Thank you, they have been merged in evolve. Sorry about the delay. On 19/05/2018 15:19, Faheem Mitha wrote: > # HG changeset patch > # User Faheem Mitha > # Date 1526734596 -19800 > #

[PATCH evolve-ext] debian: add line to clean-docs target to delete additional docs file

# HG changeset patch # User Faheem Mitha # Date 1526734596 -19800 # Sat May 19 18:26:36 2018 +0530 # Branch stable # Node ID 31a5c06bea822b58db8d77d23edea7832ae301c5 # Parent 4a70392f1723c9e31d8b7fa68b2fc942d024901d debian: add line to clean-docs target to delete