You cannot select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

Eli Barzilay d64c87af39 The Scribble reader was improved to make it pull out the syntax ... punctuations outside of the form, as it does with quote punctuations. So things like this #, @foo{...} that required the space to make the @foo read as a scribble form are now better written as @#,foo{...} This changes all such occurrences. (In case you see this change in your files and are worried that there might be changes: I mechanically verified that the result of `read'ing the modified files is identical to the previous version.) svn: r15111 original commit: 4288c6c2c703664b6bbd4cd06bd7c2160985b00d		15 years ago
collects	The Scribble reader was improved to make it pull out the syntax	15 years ago