Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Do not escape quotes in verbatim LPDoc documentation.
This confuses my text editor and I think this is actually useless. Indeed, looking at the code of Elpi seems to indicate that we do not need one additional level of escaping there.
- Loading branch information