diff options
| -rwxr-xr-x | distrib/mkDocs/mkDocs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/distrib/mkDocs/mkDocs b/distrib/mkDocs/mkDocs index fbb0a6f67a..d185b43e61 100755 --- a/distrib/mkDocs/mkDocs +++ b/distrib/mkDocs/mkDocs @@ -40,7 +40,7 @@ do done mv index.html ../../../../.. cd .. -mv *.pdf *.ps ../../../.. +mv *.pdf ../../../.. cd ../../../.. [ "$NO_CLEAN" -eq 0 ] && rm -r inst [ "$NO_CLEAN" -eq 0 ] && rm -r windows |