Merge pull request #110512 from neosimsim/agda-dont-install-Everything
Agda don't install Everything module
This commit is contained in:
@@ -23,6 +23,13 @@ in
|
||||
};
|
||||
|
||||
testScript = ''
|
||||
assert (
|
||||
"${pkgs.agdaPackages.lib.interfaceFile "Everything.agda"}" == "Everything.agdai"
|
||||
), "wrong interface file for Everything.agda"
|
||||
assert (
|
||||
"${pkgs.agdaPackages.lib.interfaceFile "tmp/Everything.agda.md"}" == "tmp/Everything.agdai"
|
||||
), "wrong interface file for tmp/Everything.agda.md"
|
||||
|
||||
# Minimal script that typechecks
|
||||
machine.succeed("touch TestEmpty.agda")
|
||||
machine.succeed("agda TestEmpty.agda")
|
||||
|
||||
Reference in New Issue
Block a user