diff options
Diffstat (limited to 'obsolete/support/detex/Flex-patch')
-rw-r--r-- | obsolete/support/detex/Flex-patch | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/obsolete/support/detex/Flex-patch b/obsolete/support/detex/Flex-patch new file mode 100644 index 0000000000..dd12337433 --- /dev/null +++ b/obsolete/support/detex/Flex-patch @@ -0,0 +1,9 @@ +From the DeTeX Home Page... + +Flex patch + +This patch has been incorporated into detex 2.7, so it is no longer +necessary. However, if you are using flex, you'll probably need to +change the link line in the make file to be + + ${CC} ${CFLAGS} -o $@ ${D_OBJ} -lfl |