summaryrefslogtreecommitdiff
path: root/.gitmodules
diff options
context:
space:
mode:
authorNadrieril2020-05-17 17:05:25 +0100
committerGitHub2020-05-17 17:05:25 +0100
commitaaba9f7a1a6119443aa6a569e451e0e549e5bb37 (patch)
tree5672d51e4197ae465b19222abb1dfca9d7e0040f /.gitmodules
parentfcce380d5b4588dc5934bc2e5448d1d981761b50 (diff)
parent6c26ae4aa828b8054b307033dc58a6dfb4dac1a0 (diff)
Merge pull request #165 from fteychene/feat/resolve_cache
Diffstat (limited to '')
-rw-r--r--.gitmodules1
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