diff --git a/ChangeLog b/ChangeLog index fc1664658..7f215dfe9 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,8 @@ 2005-02-04 Alexandre Duret-Lutz + * src/tgbaalgos/emptiness_stats.hh (unsigned_statistics::stats_map_): + Use char_ptr_less_than. + * src/misc/ltstr.hh: New file. * src/misc/Makefile.am (misc_HEADERS): Add it. diff --git a/src/tgbaalgos/emptiness_stats.hh b/src/tgbaalgos/emptiness_stats.hh index 324b73c9e..5fe9f9b8a 100644 --- a/src/tgbaalgos/emptiness_stats.hh +++ b/src/tgbaalgos/emptiness_stats.hh @@ -24,6 +24,7 @@ #include #include +#include "misc/ltstr.hh" namespace spot { @@ -50,7 +51,8 @@ namespace spot protected: typedef unsigned (unsigned_statistics::*unsigned_fun_)() const; - typedef std::map stats_map_; + typedef std::map stats_map_; stats_map_ stats_; };