From f179ae0dfb7c0b2596ef02647e02589d22a9828f Mon Sep 17 00:00:00 2001 From: Mylloon Date: Fri, 21 Oct 2022 15:38:21 +0200 Subject: [PATCH] add cmi files --- .unison/default.prf | 1 + 1 file changed, 1 insertion(+) diff --git a/.unison/default.prf b/.unison/default.prf index 9ecb9f2..f192f31 100644 --- a/.unison/default.prf +++ b/.unison/default.prf @@ -23,3 +23,4 @@ ignore = Name *.nav ignore = Name *.snm ignore = Name *.vrb ignore = Name *.o +ignore = Name *.cmi