diff options
| author | lloyd <[email protected]> | 2011-03-21 12:46:36 +0000 |
|---|---|---|
| committer | lloyd <[email protected]> | 2011-03-21 12:46:36 +0000 |
| commit | 4c5deb8796f011adead3be867d36c679d761aacf (patch) | |
| tree | 6355c391d980b04459d2eac702d6d631435f9ab7 | |
| parent | 588188b3e0c87b3f0950180169d243aa5af86d06 (diff) | |
Just use the plain text
| -rwxr-xr-x | doc/scripts/dist.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/scripts/dist.sh b/doc/scripts/dist.sh index 479de24d1..6dffb9ac4 100755 --- a/doc/scripts/dist.sh +++ b/doc/scripts/dist.sh @@ -41,7 +41,8 @@ do rm -f $doc.aux $doc.log $doc.dvi $doc.toc done -botan_log_to_html log.txt > ../../log.html +#botan_log_to_html log.txt > ../../log.html +cp log.txt ../../log.txt cd .. # topdir cd .. # now in DIST_DIR |