diff --git a/crates/docs/src/static/styles.css b/crates/docs/src/static/styles.css index dc1f934e93..3c73586699 100644 --- a/crates/docs/src/static/styles.css +++ b/crates/docs/src/static/styles.css @@ -468,6 +468,12 @@ pre { line-height: 15px; } +.builtins-tip { + padding: 1em; + font-style: italic; + line-height: 1.3em; +} + @media (prefers-color-scheme: dark) { :root { --body-bg-color: var(--purple-8); diff --git a/crates/reporting/src/report.rs b/crates/reporting/src/report.rs index 50ca390a12..80ddfc7c33 100644 --- a/crates/reporting/src/report.rs +++ b/crates/reporting/src/report.rs @@ -275,7 +275,7 @@ pub const ANSI_STYLE_CODES: StyleCodes = StyleCodes { macro_rules! html_color { ($name: expr) => { - concat!("") + concat!("") }; } @@ -287,8 +287,8 @@ pub const HTML_STYLE_CODES: StyleCodes = StyleCodes { magenta: html_color!("magenta"), cyan: html_color!("cyan"), white: html_color!("white"), - bold: "", - underline: "", + bold: "", + underline: "", reset: "", color_reset: "", }; diff --git a/www/build.sh b/www/build.sh index 73aeafe104..38ab96db1f 100755 --- a/www/build.sh +++ b/www/build.sh @@ -56,7 +56,7 @@ mv generated-docs/*.* www/build # move all the .js, .css, etc. files to build/ mv generated-docs/ www/build/builtins # move all the folders to build/builtins/ # Manually add this tip to all the builtin docs. -find www/build/builtins -type f -name 'index.html' -exec sed -i 's!!
Tip: Some names differ from other languages.
!' {} \; +find www/build/builtins -type f -name 'index.html' -exec sed -i 's!!
Tip: Some names differ from other languages.
!' {} \; echo 'Generating CLI example platform docs...' # Change ROC_DOCS_ROOT_DIR=builtins so that links will be generated relative to diff --git a/www/public/repl/repl.css b/www/public/repl/repl.css index bbf6d1a6f6..cee0b97bf9 100644 --- a/www/public/repl/repl.css +++ b/www/public/repl/repl.css @@ -75,3 +75,31 @@ section.source textarea { padding: 8px; margin-bottom: 16px; } + +.color-red { + color: red; +} +.color-green { + color: green; +} +.color-yellow { + color: yellow; +} +.color-blue { + color: blue; +} +.color-magenta { + color: magenta; +} +.color-cyan { + color: cyan; +} +.color-white { + color: white; +} +.bold { + font-weight: bold; +} +.underline { + text-decoration: underline; +} \ No newline at end of file