From 6a5dcbbfea1af0308a4d49e7c5bcea26d74a739d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 31 May 2019 13:09:23 +0200
Subject: Remove Show Script (deprecated in 8.10)

---
 dev/v8-syntax/syntax-v8.tex | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev')

diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index dd3908c25f..601d52ddda 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -1167,7 +1167,6 @@ $$
 \nlsep \TERM{Show}~\OPT{\NT{num}}
 \nlsep \TERM{Show}~\TERM{Implicit}~\TERM{Arguments}~\OPT{\NT{num}}
 \nlsep \TERM{Show}~\TERM{Node}
-\nlsep \TERM{Show}~\TERM{Script}
 \nlsep \TERM{Show}~\TERM{Existentials}
 \nlsep \TERM{Show}~\TERM{Tree}
 \nlsep \TERM{Show}~\TERM{Conjecture}
-- 
cgit v1.2.3