diff options
| -rw-r--r-- | otherlibs/labltk/labltk/.ignore | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/otherlibs/labltk/labltk/.ignore b/otherlibs/labltk/labltk/.ignore index b8fc4134f..81bd183eb 100644 --- a/otherlibs/labltk/labltk/.ignore +++ b/otherlibs/labltk/labltk/.ignore @@ -2,4 +2,3 @@ *.mli labltktop labltk -modules |