On 19 Feb 2015 23:31, Jiri Gaisler wrote:
> 	Use gdb's readline.h for readline types.

merged, thanks !
-mike