diff --git a/gitlab-pages/website/static/css/custom.css b/gitlab-pages/website/static/css/custom.css index b753ec486..db72d3906 100644 --- a/gitlab-pages/website/static/css/custom.css +++ b/gitlab-pages/website/static/css/custom.css @@ -939,3 +939,18 @@ a:hover { width: 15em; } } + + +/* ReasonLIGO specific syntax highlighting */ +.language-reasonligo .hljs-operator { + color: #a626a4; +} +.language-reasonligo .hljs-character { + color: #50a14f; +} +.language-reasonligo .hljs-module-identifier { + color: #4078f2; +} +.language-reasonligo .hljs-constructor { + color: #e45649; +} \ No newline at end of file