diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-02-14 15:52:12 +0100 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-02-14 15:52:12 +0100 |
| commit | 3dc547c3e3e7279085b4807c551f327c5b985a49 (patch) | |
| tree | e85a8fcd5dbbe04b4afddf2426031560b217946e /reproduce/src/make | |
| parent | 3d216bd6797bc4bf0d02cd43adf37706b057c580 (diff) | |
Some extra space in alert when no PDF is created
To help view that everything is OK and that there were no errors, an extra
blank line followed by one with `----' is added to the notice when we won't
be making a PDF. These two lines help the eye more clearly see everything
is fine (given that above it, there are MANY commands and outputs).
Diffstat (limited to 'reproduce/src/make')
0 files changed, 0 insertions, 0 deletions