From: John Darrington <john@darrington.wattle.id.au>
Date: Tue, 8 Dec 2015 14:56:13 +0000 (+0100)
Subject: Fix generation of help-pages-list file
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=65dea0d51ec33cbc614a3ec87b5aae28c86f005a;hp=65dea0d51ec33cbc614a3ec87b5aae28c86f005a;p=pspp

Fix generation of help-pages-list file
---