diff options
| author | Benjamin Pierce <bcpierce00@users.noreply.github.com> | 2018-02-09 12:46:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-09 12:46:52 -0500 |
| commit | 3f36a21bfea40aa08f8d25f96dd1d10f8be05284 (patch) | |
| tree | 33cf7247f56dda9049fd4d3c8926de4960c47e5c | |
| parent | c40073637d026da5fb51b3858b859ed8414b65ec (diff) | |
| download | unison-3f36a21bfea40aa08f8d25f96dd1d10f8be05284.zip unison-3f36a21bfea40aa08f8d25f96dd1d10f8be05284.tar.gz unison-3f36a21bfea40aa08f8d25f96dd1d10f8be05284.tar.bz2 | |
Update trace.ml
| -rw-r--r-- | src/ubase/trace.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ubase/trace.ml b/src/ubase/trace.ml index 3c5696d..d47054a 100644 --- a/src/ubase/trace.ml +++ b/src/ubase/trace.ml @@ -117,7 +117,7 @@ let logfile = "!logfile name" "By default, logging messages will be appended to the file \\verb|unison.log| in your HOME directory. Set this preference if - you prefer another file. It can be relative to your HOME directory." + you prefer another file. It can be a path relative to your HOME directory." let logch = ref None |