From 06f07109a4e797d584c0aa50fd6221fdb1843327 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Feb 2005 11:49:16 +0000 Subject: [PATCH] removed chosenTransformer.mli --- helm/gTopLevel/Makefile.in | 1 - 1 file changed, 1 deletion(-) diff --git a/helm/gTopLevel/Makefile.in b/helm/gTopLevel/Makefile.in index 75340e3aa..b64716cc2 100644 --- a/helm/gTopLevel/Makefile.in +++ b/helm/gTopLevel/Makefile.in @@ -43,7 +43,6 @@ INTERFACE_FILES = \ disambiguatingParser.mli \ termEditor.mli \ texTermEditor.mli \ - chosenTransformer.mli \ termViewer.mli \ invokeTactics.mli \ hbugs.mli \ -- 2.39.2