Links to online documentation:

* Adding a help button on top of the chat, that links to the online documentation on frama.io.
* Replaced github.io documentation links by frama.io documentation.
* Adding links to the documentation in the diagnostic tool.
This commit is contained in:
John Livingston
2023-07-26 18:16:30 +02:00
parent 8db4f10584
commit 3fd6b9b563
12 changed files with 199 additions and 28 deletions

View File

@ -1,6 +1,10 @@
interface MessageWithLevel {
level: 'info' | 'warning' | 'error'
message: string
help?: {
url: string
text: string
}
}
interface Result {
@ -63,8 +67,15 @@ function launchTests (): void {
} else if (message.level === 'error') {
messageSpan.style.color = 'red'
}
messageSpan.textContent = message.message
messageSpan.textContent = message.message + ' ' // adding a space, in case there is a help button
messageLi.append(messageSpan)
if (message.help) {
const helpButton = document.createElement('a')
helpButton.href = message.help.url
helpButton.textContent = message.help.text
messageLi.append(helpButton)
}
}
messageUl.append(messageLi)
}