diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/language/Makefile b/language/Makefile index 081d90a7..759523b7 100644 --- a/language/Makefile +++ b/language/Makefile @@ -1,6 +1,6 @@ #OTT=../../../rsem/ott/bin/ott # this is the binary that gets rebuilt by make in ott/src: -OTT=../../../github/ott/src/ott +OTT=../../ott/src/ott OTTLIB=$(dir $(shell which ott))../hol .PHONY: all |