diff options
| -rw-r--r-- | doc/old/banner.tex (renamed from doc/banner.tex) | 0 | ||||
| -rw-r--r-- | doc/old/status.tex (renamed from doc/status.tex) | 0 |
2 files changed, 0 insertions, 0 deletions
diff --git a/doc/banner.tex b/doc/old/banner.tex index e1170562..e1170562 100644 --- a/doc/banner.tex +++ b/doc/old/banner.tex diff --git a/doc/status.tex b/doc/old/status.tex index cd7ce897..cd7ce897 100644 --- a/doc/status.tex +++ b/doc/old/status.tex |