From f09a92345c38e950b898677f5197c90e4f905389 Mon Sep 17 00:00:00 2001 From: leonv Date: Wed, 20 Mar 2024 15:51:21 +0100 Subject: [PATCH] Update .gitattributes --- .gitattributes | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.gitattributes b/.gitattributes index 6105c25..2997552 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1,4 +1,3 @@ *.lagda.md linguist-language=Agda *.lagda.md linguist-detectable=true - -*.css linguist-detectable=false +agda/Agda.css linguist-vendored