diff options
Diffstat (limited to 'Build/source/texk/detex/detex-2.8/detex.l')
-rw-r--r-- | Build/source/texk/detex/detex-2.8/detex.l | 2 |
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 $"; |