diff options
| -rw-r--r-- | Doc/dist/dist.tex | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Doc/dist/dist.tex b/Doc/dist/dist.tex index aa063f93d4..32a39c1bed 100644 --- a/Doc/dist/dist.tex +++ b/Doc/dist/dist.tex @@ -866,6 +866,8 @@ version. This information includes: {URL}{(4)} \lineiv{classifiers}{a list of classifiers} {list of strings}{(4)} + \lineiv{platforms}{a list of platforms} + {list of strings}{} \end{tableiv} \noindent Notes: |