diff options
| author | Felix Mulder <felix.mulder@gmail.com> | 2017-01-23 17:17:55 +0100 |
|---|---|---|
| committer | Felix Mulder <felix.mulder@gmail.com> | 2017-01-31 14:32:41 +0100 |
| commit | f56a8b3246adca23ed76beefb0eb5102e70f6d97 (patch) | |
| tree | 80dbe287197d6a795d805217cf57949f03814346 /docs | |
| parent | dc4bd3d69c1671036dd85be5311c52fd0bc85c4f (diff) | |
| download | dotty-f56a8b3246adca23ed76beefb0eb5102e70f6d97.tar.gz dotty-f56a8b3246adca23ed76beefb0eb5102e70f6d97.tar.bz2 dotty-f56a8b3246adca23ed76beefb0eb5102e70f6d97.zip | |
Add @OlivierBlanvillain to the core devs
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/_includes/faq.html | 8 | ||||
| -rw-r--r-- | docs/_includes/features.html | 8 | ||||
| -rw-r--r-- | docs/images/olivier.jpeg | bin | 0 -> 10202 bytes | |||
| -rw-r--r-- | docs/index.html | 1 |
4 files changed, 13 insertions, 4 deletions
diff --git a/docs/_includes/faq.html b/docs/_includes/faq.html index 7c2126ac4..569162d57 100644 --- a/docs/_includes/faq.html +++ b/docs/_includes/faq.html @@ -86,6 +86,14 @@ Nicolas Stucki </div> </div> + <div class="contributors-cell"> + <div class="contributor"> + <a href="http://github.com/OlivierBlanvillain"> + <img src="{{ site.baseurl }}/images/olivier.jpeg"> + </a> + Olivier Blanvillain + </div> + </div> </div> <div class="centered-text"> diff --git a/docs/_includes/features.html b/docs/_includes/features.html index ba004d68b..0f8d4eab2 100644 --- a/docs/_includes/features.html +++ b/docs/_includes/features.html @@ -69,12 +69,12 @@ <td>In progress</td> </tr> <tr class="even"> - <td></td> - <td></td> + <td>HList & HMaps/Record types</td> + <td>In progress</td> </tr> <tr class="odd"> - <td>HList & HMaps/Record types</td> - <td>Considered</td> + <td></td> + <td></td> </tr> <tr class="even"> <td>Implicit functions</td> diff --git a/docs/images/olivier.jpeg b/docs/images/olivier.jpeg Binary files differnew file mode 100644 index 000000000..7c11e1de3 --- /dev/null +++ b/docs/images/olivier.jpeg diff --git a/docs/index.html b/docs/index.html index 5870c5994..7e9ed7717 100644 --- a/docs/index.html +++ b/docs/index.html @@ -1,4 +1,5 @@ --- +title: Dotty layout: main extraCSS: - css/animate.css |
