io: fix stream-copy docs.

char-rename
John Benediktsson 2017-01-24 20:40:29 -08:00
parent 1829c73bb1
commit 09f11e293a
1 changed files with 4 additions and 2 deletions

View File

@ -486,8 +486,10 @@ $nl
each-block each-block
} }
"Copying the contents of one stream to another:" "Copying the contents of one stream to another:"
{ $subsections stream-copy* } { $subsections
{ $subsections stream-copy } ; stream-copy*
stream-copy
} ;
ARTICLE: "stream-examples" "Stream example" ARTICLE: "stream-examples" "Stream example"
"Ask the user for their age, and print it back:" "Ask the user for their age, and print it back:"