From fc048a338ecaac55f12a2a27ef32f9e4c2ab5db6 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 3 Feb 2006 16:15:32 +0000 Subject: [PATCH] removed no longer needed libs link --- helm/libs | 1 - 1 file changed, 1 deletion(-) delete mode 120000 helm/libs diff --git a/helm/libs b/helm/libs deleted file mode 120000 index 5074bc27f..000000000 --- a/helm/libs +++ /dev/null @@ -1 +0,0 @@ -ocaml/ \ No newline at end of file -- 2.39.5