[server] Information: adds an optional longer description, shown as title.
[descr] is used in the dropdown list of information kinds. [title] is used as tooltip on the information.
Showing
- ivette/src/frama-c/kernel/ASTinfo.tsx 7 additions, 9 deletionsivette/src/frama-c/kernel/ASTinfo.tsx
- ivette/src/frama-c/kernel/Properties.tsx 2 additions, 2 deletionsivette/src/frama-c/kernel/Properties.tsx
- ivette/src/frama-c/kernel/api/ast/index.ts 4 additions, 3 deletionsivette/src/frama-c/kernel/api/ast/index.ts
- src/plugins/eva/api/general_requests.ml 1 addition, 1 deletionsrc/plugins/eva/api/general_requests.ml
- src/plugins/server/kernel_ast.ml 10 additions, 7 deletionssrc/plugins/server/kernel_ast.ml
- src/plugins/server/kernel_ast.mli 5 additions, 3 deletionssrc/plugins/server/kernel_ast.mli
Loading
Please register or sign in to comment