[paparazzi-commits] [paparazzi/paparazzi] 7f72fc: paparazzicenter: green background color for info m...

[GitHub]

  Branch: refs/heads/dev
  Home:   https://github.com/paparazzi/paparazzi
  Commit: 7f72fcd2cd332aa2b5e943eb69a50da7a4daa1b4
      
https://github.com/paparazzi/paparazzi/commit/7f72fcd2cd332aa2b5e943eb69a50da7a4daa1b4
  Author: Felix Ruess <address@hidden>
  Date:   2012-02-12 (Sun, 12 Feb 2012)

  Changed paths:
    M sw/supervision/paparazzicenter.ml

  Log Message:
  -----------
  paparazzicenter: green background color for info messages (e.g. via #pragma 
message)


  Commit: 9ba1f61ff5ffd807fddf190d5b60d68b3c8a7206
      
https://github.com/paparazzi/paparazzi/commit/9ba1f61ff5ffd807fddf190d5b60d68b3c8a7206
  Author: Felix Ruess <address@hidden>
  Date:   2012-02-12 (Sun, 12 Feb 2012)

  Changed paths:
    M sw/supervision/paparazzicenter.ml

  Log Message:
  -----------
  Merge branch 'master' into dev


Compare: https://github.com/paparazzi/paparazzi/compare/0d99fa2...9ba1f61