diff options
author | Nadrieril | 2020-05-17 17:05:25 +0100 |
---|---|---|
committer | GitHub | 2020-05-17 17:05:25 +0100 |
commit | aaba9f7a1a6119443aa6a569e451e0e549e5bb37 (patch) | |
tree | 5672d51e4197ae465b19222abb1dfca9d7e0040f /.gitmodules | |
parent | fcce380d5b4588dc5934bc2e5448d1d981761b50 (diff) | |
parent | 6c26ae4aa828b8054b307033dc58a6dfb4dac1a0 (diff) |
Merge pull request #165 from fteychene/feat/resolve_cache
Diffstat (limited to '')
-rw-r--r-- | .gitmodules | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitmodules b/.gitmodules index 16b16c4..81e455f 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,4 @@ [submodule "dhall-lang"] path = dhall-lang url = https://github.com/dhall-lang/dhall-lang + ignore = dirty |