diff options
| author | Jim Fehrle | 2020-04-17 12:26:28 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-04-19 09:27:28 -0700 |
| commit | 796878d827693fefdfe4901af7a71bfe20f2011c (patch) | |
| tree | 83469fd75716a662bdebd6455071856d705013b3 /doc/common/styles/html/coqremote/modules/node/node.css | |
| parent | f3af9a4c6e6813f32dfe632209e145ffbf5fed98 (diff) | |
Don't create index entries for the name "_"
Diffstat (limited to 'doc/common/styles/html/coqremote/modules/node/node.css')
0 files changed, 0 insertions, 0 deletions