docs update stale code_listing docstring

Remove reference to 'progressive enhancement layered on top' which described the now-removed highlight.js integration. The plain code_listing now simply renders uncoloured text; for highlighting, callers should use highlighted_code_listing.

Commit
8b1ea92f220320b8fafbdc6497b886e09a578837
Author
Marius Peter <dev@marius-peter.com>
Author date
Committer
Marius Peter <dev@marius-peter.com>
Committer date
lib/views/ui.mli
index da2d15cb..688aeca8 100644..100644
@@ -303,8 +303,8 @@
303 303 highlighted. [anchor_prefix] namespaces those anchors, which is required
304 304 when one page shows more than one listing.
305 305
306 Removed: Content is emitted verbatim as text; syntax colouring, if any, is a
307 Removed: progressive enhancement layered on top. *)
306 Added: Content is emitted verbatim as plain text with no syntax colouring.
307 Added: For highlighted output, use {!highlighted_code_listing} instead. *)
308 308
309 309 val highlighted_code_listing :
310 310 ?id:string -> ?class_:string -> ?anchor_prefix:string -> node list list -> node