From e0c6872cf40896c7be36b11dcc744620f10adf1d Mon Sep 17 00:00:00 2001 From: Norbert Preining Date: Mon, 2 Sep 2019 13:46:59 +0900 Subject: Initial commit --- web/spiderweb/patches/008 | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 web/spiderweb/patches/008 (limited to 'web/spiderweb/patches/008') diff --git a/web/spiderweb/patches/008 b/web/spiderweb/patches/008 new file mode 100644 index 0000000000..d0e0615e3a --- /dev/null +++ b/web/spiderweb/patches/008 @@ -0,0 +1,29 @@ +*** c/c.spider.old Wed Nov 29 22:48:59 1989 +--- c/c.spider Wed Nov 29 21:55:48 1989 +*************** +*** 18,28 **** + + token + category unorbinop + token - category unorbinop +! token * category unorbinop translation <"{*}"> + token / category dot + token < category less translation <> + token > category greater translation <> + token = category equals translation <"\\leftarrow"> tangleto <"="-space> + token . category dot + token ~ category unop translation <"\\TI"> + token & category unorbinop translation <"\\amp"> +--- 18,30 ---- + + token + category unorbinop + token - category unorbinop +! token * category unorbinop translation <"{*}"> tangleto +! # avoid inadvertant /* + token / category dot + token < category less translation <> + token > category greater translation <> + token = category equals translation <"\\leftarrow"> tangleto <"="-space> ++ # avoid inadvertant =- + token . category dot + token ~ category unop translation <"\\TI"> + token & category unorbinop translation <"\\amp"> -- cgit v1.2.3