Skip to content

Commit 00dc06c

Browse files
gallaisgallais
committed
[ admin ] dev playground
1 parent 3a1bda2 commit 00dc06c

File tree

3 files changed

+9
-0
lines changed

3 files changed

+9
-0
lines changed

‎dev/.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
*

‎dev/README.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
# Development playground
2+
3+
This directory allows you to develop modules against the current dev
4+
version of the stdlib as it currently sits in `src/`.

‎dev/experimental.agda-lib

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
name: standard-library-dev
2+
include: . ../src
3+
flags:
4+
--warning=noUnsupportedIndexedMatch

0 commit comments

Comments
 (0)