*
* Prints a null-terminated string to the current stream. It is exactly
* equivalent to
- * <informalexample><programlisting>
+ * |[
* for (ptr = @s; *ptr; ptr++)
* #glk_put_char(*ptr);
- * </programlisting></informalexample>
+ * ]|
* However, it may be more efficient.
*/
void
*
* Prints a block of characters to the current stream. It is exactly equivalent
* to:
- * <informalexample><programlisting>
+ * |[
* for (i = 0; i < @len; i++)
* #glk_put_char(@buf[i]);
- * </programlisting></informalexample>
+ * ]|
* However, it may be more efficient.
*/
void