Add test3 to ignored_subdirs.

cknitt · cknitt · commit 88204eaab2d5 · 2018-11-17T13:37:39.000+01:00
diff --git a/test/dune b/test/dune
@@ -1,4 +1,4 @@
-(ignored_subdirs (test1 test2))
+(ignored_subdirs (test1 test2 test3))
 
 (executable
   (name Test)

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-(ignored_subdirs (test1 test2))`
	`1`	`+(ignored_subdirs (test1 test2 test3))`
`2`	`2`
`3`	`3`	`(executable`
`4`	`4`	`(name Test)`