summaryrefslogtreecommitdiff
path: root/Build/source/texk/detex/detex-2.8/detex.l
diff options
context:
space:
mode:
Diffstat (limited to 'Build/source/texk/detex/detex-2.8/detex.l')
-rw-r--r--Build/source/texk/detex/detex-2.8/detex.l2
1 files changed, 2 insertions, 0 deletions
diff --git a/Build/source/texk/detex/detex-2.8/detex.l b/Build/source/texk/detex/detex-2.8/detex.l
index 7ace6f49ac3..7b4aaa1a1de 100644
--- a/Build/source/texk/detex/detex-2.8/detex.l
+++ b/Build/source/texk/detex/detex-2.8/detex.l
@@ -1,3 +1,5 @@
+%option never-interactive
+
%{
#ifndef lint
static char rcsid[] = "$Header: /p/src/local/bin/detex/RCS/detex.l,v 2.22 2007/03/01 20:22:01 trinkle Exp trinkle $";