From b6028b5bb32e553d2f1497298697e5c4deedf648 Mon Sep 17 00:00:00 2001 From: Han-Wen Nienhuys Date: Wed, 28 May 2008 23:14:56 -0300 Subject: [PATCH] Require log file if -dseparate-log-files is specified. --- scripts/lilypond-book.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/lilypond-book.py b/scripts/lilypond-book.py index 649d660da5..63f075a149 100644 --- a/scripts/lilypond-book.py +++ b/scripts/lilypond-book.py @@ -1207,6 +1207,8 @@ class LilypondSnippet (Snippet): if 'ddump-profile' in global_options.process_cmd: require_file (base + '.profile') + if 'dseparate-log-file' in global_options.process_cmd: + require_file (base + '.log') map (consider_file, [base + '.tex', base + '.eps', -- 2.39.2