diff options
Diffstat (limited to 'src/config_file.ml')
| -rw-r--r-- | src/config_file.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/config_file.ml b/src/config_file.ml index efb6fb3..69c47db 100644 --- a/src/config_file.ml +++ b/src/config_file.ml @@ -21,6 +21,7 @@ let read dir = match words line with | [ "Basedir"; ".." ] -> { basedir = Some 1 } | [ "Basedir"; "../.." ] -> { basedir = Some 2 } + | [ "Basedir"; "../../.." ] -> { basedir = Some 3 } | [] -> config (* blank line *) | [ "Ignore"; pkg ] | [ pkg ] (* the deprecated form *) |