Remove pointless logging directives in regression2
commit6dca7b8a185a1eddb61ef8f9109681e0c25aca02
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 22 Jan 2018, 09:30 (9 years ago)
parentfc261d6
test/regression002/reg001.idr−2
@@ -1,5 +1,3 @@
1−%logging 0
21foo : (a : Type) -> (b : Type) -> a -> b
32foo a a x = x
4−%logging 0
53