mailing-list for TeXmacs Users

[Sam Liddicott <address@hidden>]

/dev/stdout as an export filename used to export text

texmacs -s -c wfs-utils.tm /dev/stdout -q

It still does, but not in the same way it used to.

For this simple document here:

<TeXmacs|1.0.7.15>

<style|generic>

<\body>

  <assign|specific-verbatim|<macro|x|<clipped|<arg|x>|0|0|0|0>>>

  <specific-verbatim|lallallal>

</body>

If I export with this command:

texmacs -s -c x.tm /tmp/x.txt -q

Then the text file contains the text: lallallal

If I export with either of these commands:

texmacs -s -c x.tm /tmp/x -q

texmacs -s -c x.tm /dev/stdout -q

Then the text file contains nothing. This breaks my literate programming makefiles. I can work around it but I wonder: 

What is this secret extra export option which looks like text but isn't quite?

I also draw attention to the fact that I need the specific-verbatim macro that uses <clipped|...> because the <specific|...> tag does not accept verbatim as an option and I require to be able to select a suitable text representation for some items during text export.