diff options
Diffstat (limited to 'src/third_party/wiredtiger/src/docs/tools/doxfilter.py')
| -rwxr-xr-x | src/third_party/wiredtiger/src/docs/tools/doxfilter.py | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/third_party/wiredtiger/src/docs/tools/doxfilter.py b/src/third_party/wiredtiger/src/docs/tools/doxfilter.py index a84723be0ec..39c48d75011 100755 --- a/src/third_party/wiredtiger/src/docs/tools/doxfilter.py +++ b/src/third_party/wiredtiger/src/docs/tools/doxfilter.py @@ -79,6 +79,7 @@ def process_arch(source): result += '@arch_page_table{' + \ data_structures_str + ',' + \ files_str + '}\n' + result += '@arch_page_caution\n' else: result += line + '\n' return result |