Skip to content

Commit 6299194

Browse files
committed
resolve issue with extra main entry point in dotnet
1 parent f8e5ac3 commit 6299194

File tree

2 files changed

+2
-4
lines changed

2 files changed

+2
-4
lines changed

.github/workflows/ci_test_vector_net.yml

+2
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,8 @@ jobs:
5252
shell: bash
5353
working-directory: ./TestVectors
5454
run: |
55+
# this is evil, but the MPL test vectors defines an extra Main
56+
sed -i '' 's/method Main/method NotMain/' ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy
5557
# This works because `node` is installed by default on GHA runners
5658
make transpile_net
5759

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

-4
Original file line numberDiff line numberDiff line change
@@ -31,12 +31,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
3131
import DDB = ComAmazonawsDynamodbTypes
3232
import Filter = DynamoDBFilterExpr
3333
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
34-
import SKS = CreateStaticKeyStores
35-
import KeyMaterial
3634
import UTF8
37-
import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
3835
import CMP = AwsCryptographyMaterialProvidersTypes
39-
import KeyVectors
4036
import CreateInterceptedDDBClient
4137
import SortedSets
4238
import Seq

0 commit comments

Comments
 (0)