Wilfred Hughes dda641c62c Set documentation field in SCIP from doc comment
Previously, the documentation field was the same as the text shown to
users when they hover over that symbol. The documentation should
really just be the doc comment, and as of #16179 the signature is
already stored in the signatureDocumentation field.
2024-02-14 14:46:32 -08:00
..