diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Makefile b/src/Makefile index 784ae1a..7bc09bb 100644 --- a/src/Makefile +++ b/src/Makefile @@ -338,7 +338,7 @@ testmerge: .PHONY: tags tags: - -if [ -f `which $(ETAGS)` ]; then \ + -if [ -f "`which $(ETAGS)`" ]; then \ $(ETAGS) *.mli */*.mli *.ml */*.ml */*.m *.c */*.c *.txt \ ; fi |