added comment about version number to be manually changed

[helm.git] / matita / components / ng_disambiguation / Makefile

diff --git a/matita/components/ng_disambiguation/Makefile b/matita/components/ng_disambiguation/Makefile
index 8c564325e6e069894d7db3805651981b0e33622b..082d000bc7b1675c5083c69378ab6d53c62d411d 100644 (file)
--- a/matita/components/ng_disambiguation/Makefile
+++ b/matita/components/ng_disambiguation/Makefile
@@ -2,9 +2,9 @@ PACKAGE = ng_disambiguation
 PREDICATES =
 
 INTERFACE_FILES =              \
+       nnumber_notation.mli    \
        disambiguateChoices.mli \
   nCicDisambiguate.mli    \
-       nnumber_notation.mli    \
        grafiteDisambiguate.mli \
        $(NULL)
 IMPLEMENTATION_FILES =         \