From 62e2033025d530d0b8b40c827e545656f41c3935 Mon Sep 17 00:00:00 2001 From: totoro Date: Sat, 6 Jul 2019 13:36:37 +0200 Subject: [PATCH] helper for href with only one extra operand --- web/types/making_a_web_site.anubis | 9 +++++++++ 1 file changed, 9 insertions(+), 0 deletions(-) diff --git a/web/types/making_a_web_site.anubis b/web/types/making_a_web_site.anubis index 49ef7bb..0358c83 100644 --- a/web/types/making_a_web_site.anubis +++ b/web/types/making_a_web_site.anubis @@ -408,6 +408,15 @@ public type A_href: href(WEB_Action_Name action, List((String,String)) extra_ops) . +public define A_href + href + ( + WEB_Action_Name action, + (String,String) extra_ops + )= + href(action, [extra_ops]) +. + public type A_target: _blank, _self, -- libgit2 0.21.4