Confirmed users
574
edits
DXR Parallel Tree Indexing: Difference between revisions
Jump to navigation
Jump to search
Add generated_date.
(Add description to frozen config.) |
(Add generated_date.) |
||
| Line 21: | Line 21: | ||
description: "Some tree", # needed so new trees or edited descriptions can show up without a WSGI restart | description: "Some tree", # needed so new trees or edited descriptions can show up without a WSGI restart | ||
enabled_plugins: ["clang", "pygmentize"], | enabled_plugins: ["clang", "pygmentize"], | ||
generated_date: "2012-05-02 11:04:50", | |||
maybe some plugin config # TODO: how do we pluggably serialize this? We don't need any of these yet, so it can wait. | maybe some plugin config # TODO: how do we pluggably serialize this? We don't need any of these yet, so it can wait. | ||
} | } | ||