diff options
Diffstat (limited to 'web')
| -rw-r--r-- | web/website.ini | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/web/website.ini b/web/website.ini index 32b1936d5..273c3223d 100644 --- a/web/website.ini +++ b/web/website.ini @@ -51,6 +51,7 @@ srcdoc2: "pure/ropes;pure/unidecode/unidecode;pure/xmldom;pure/xmldomparser" srcdoc2: "pure/xmlparser;pure/htmlparser;pure/xmltree;pure/colors;pure/mimetypes" srcdoc2: "pure/json;pure/base64;pure/scgi" srcdoc2: "pure/collections/tables;pure/collections/sets;pure/collections/lists" +srcdoc2: "pure/collections/sharedlist;pure/collections/sharedtables" srcdoc2: "pure/collections/intsets;pure/collections/queues;pure/collections/deques;pure/encodings" srcdoc2: "pure/events;pure/collections/sequtils;pure/cookies" srcdoc2: "pure/memfiles;pure/subexes;pure/collections/critbits" |