diff options
-rwxr-xr-x | docs/makedocs.pl | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/docs/makedocs.pl b/docs/makedocs.pl index d29a3fb91..deb117ff3 100755 --- a/docs/makedocs.pl +++ b/docs/makedocs.pl @@ -137,4 +137,6 @@ foreach my $lang (@langs) { say 'pdflatex or rst2pdf not found. Skipping PDF file creation'; } } + + rmtree('doctrees', 0, 1); } |