commit 6cab1610bfaa7884cc322ce9c89b254dc6b7359e · pyrox.dev/nixpkgs

+1 -2

.editorconfig

···

       23
       23
        
       

     

       24
       24
        
       # see https://nixos.org/nixpkgs/manual/#chap-conventions

     

       25
       25
        
       

     

       26
       26
       -
       # Match json/lockfiles/markdown/nix/perl/python/ruby/shell/docbook files, set indent to spaces

     

       27
       27
       -
       [*.{bash,js,json,lock,md,nix,pl,pm,py,rb,sh,xml}]

     

       26
       26
       +
       [*.{bash,css,js,json,lock,md,nix,pl,pm,py,rb,sh,xml}]

     

       28
       27
        
       indent_style = space

     

       29
       28
        
       

     

       30
       29
        
       # Match docbook files, set indent width of one

+16

ci/default.nix

···

       42
       42
        
       

     

       43
       43
        
               programs.actionlint.enable = true;

     

       44
       44
        
       

     

       45
       45
       +
               programs.biome = {

     

       46
       46
       +
                 enable = true;

     

       47
       47
       +
                 settings.formatter = {

     

       48
       48
       +
                   useEditorconfig = true;

     

       49
       49
       +
                 };

     

       50
       50
       +
                 settings.javascript.formatter = {

     

       51
       51
       +
                   quoteStyle = "single";

     

       52
       52
       +
                   semicolons = "asNeeded";

     

       53
       53
       +
                 };

     

       54
       54
       +
                 settings.json.formatter.enabled = false;

     

       55
       55
       +
               };

     

       56
       56
       +
               settings.formatter.biome.excludes = [

     

       57
       57
       +
                 "*.min.js"

     

       58
       58
       +
                 "pkgs/*"

     

       59
       59
       +
               ];

     

       60
       60
       +
       

     

       45
       61
        
               programs.keep-sorted.enable = true;

     

       46
       62
        
       

     

       47
       63
        
               # This uses nixfmt underneath,

+57 -28

ci/github-script/commits.js

···

       1
       1
       -
       module.exports = async function ({ github, context, core, dry }) {

     

       1
       1
       +
       module.exports = async ({ github, context, core, dry }) => {

     

       2
       2
        
         const { execFileSync } = require('node:child_process')

     

       3
       3
       -
         const { readFile } = require('node:fs/promises')

     

       4
       4
       -
         const { join } = require('node:path')

     

       5
       3
        
         const { classify } = require('../supportedBranches.js')

     

       6
       4
        
         const withRateLimit = require('./withRateLimit.js')

     

       7
       5
        
       

     
···

       18
       16
        
                 run_id: context.runId,

     

       19
       17
        
                 per_page: 100,

     

       20
       18
        
               })

     

       21
       21
       -
             ).find(({ name }) => name == 'Check / cherry-pick').html_url +

     

       19
       19
       +
             ).find(({ name }) => name === 'Check / cherry-pick').html_url +

     

       22
       20
        
               '?pr=' +

     

       23
       21
        
               pull_number

     

       24
       22
        
       

     

       25
       23
        
           async function extract({ sha, commit }) {

     

       26
       24
        
             const noCherryPick = Array.from(

     

       27
       27
       -
               commit.message.matchAll(/^Not-cherry-picked-because: (.*)$/g)

     

       25
       25
       +
               commit.message.matchAll(/^Not-cherry-picked-because: (.*)$/g),

     

       28
       26
        
             ).at(0)

     

       29
       27
        
       

     

       30
       28
        
             if (noCherryPick)

     
···

       148
       146
        
       

     

       149
       147
        
           const fetch = extracted

     

       150
       148
        
             .filter(({ severity }) => !severity)

     

       151
       151
       -
             .map(({ sha, original_sha }) => [ sha, original_sha ])

     

       152
       152
       -
             .flat()

     

       149
       149
       +
             .flatMap(({ sha, original_sha }) => [sha, original_sha])

     

       153
       150
        
       

     

       154
       151
        
           if (fetch.length > 0) {

     

       155
       152
        
             // Fetching all commits we need for diff at once is much faster than any other method.

     
···

       163
       160
        
             ])

     

       164
       161
        
           }

     

       165
       162
        
       

     

       166
       166
       -
           const results = extracted.map(result => result.severity ? result : diff(result))

     

       163
       163
       +
           const results = extracted.map((result) =>

     

       164
       164
       +
             result.severity ? result : diff(result),

     

       165
       165
       +
           )

     

       167
       166
        
       

     

       168
       167
        
           // Log all results without truncation, with better highlighting and all whitespace changes to the job log.

     

       169
       168
        
           results.forEach(({ sha, commit, severity, message, colored_diff }) => {

     
···

       177
       176
        
       

     

       178
       177
        
           // Only create step summary below in case of warnings or errors.

     

       179
       178
        
           // Also clean up older reviews, when all checks are good now.

     

       180
       180
       -
           if (results.every(({ severity }) => severity == 'info')) {

     

       179
       179
       +
           if (results.every(({ severity }) => severity === 'info')) {

     

       181
       180
        
             if (!dry) {

     

       182
       181
        
               await Promise.all(

     

       183
       182
        
                 (

     
···

       186
       185
        
                     pull_number,

     

       187
       186
        
                   })

     

       188
       187
        
                 )

     

       189
       189
       -
                   .filter((review) => review.user.login == 'github-actions[bot]')

     

       188
       188
       +
                   .filter((review) => review.user.login === 'github-actions[bot]')

     

       190
       189
        
                   .map(async (review) => {

     

       191
       191
       -
                     if (review.state == 'CHANGES_REQUESTED') {

     

       190
       190
       +
                     if (review.state === 'CHANGES_REQUESTED') {

     

       192
       191
        
                       await github.rest.pulls.dismissReview({

     

       193
       192
        
                         ...context.repo,

     

       194
       193
        
                         pull_number,

     
···

       214
       213
        
       

     

       215
       214
        
           // In the case of "error" severity, we also fail the job.

     

       216
       215
        
           // Those should be considered blocking and not be dismissable via review.

     

       217
       217
       -
           if (results.some(({ severity }) => severity == 'error'))

     

       216
       216
       +
           if (results.some(({ severity }) => severity === 'error'))

     

       218
       217
        
             process.exitCode = 1

     

       219
       218
        
       

     

       220
       220
       -
           core.summary.addRaw('This report is automatically generated by the `PR / Check / cherry-pick` CI workflow.', true)

     

       219
       219
       +
           core.summary.addRaw(

     

       220
       220
       +
             'This report is automatically generated by the `PR / Check / cherry-pick` CI workflow.',

     

       221
       221
       +
             true,

     

       222
       222
       +
           )

     

       221
       223
        
           core.summary.addEOL()

     

       222
       222
       -
           core.summary.addRaw("Some of the commits in this PR require the author's and reviewer's attention.", true)

     

       224
       224
       +
           core.summary.addRaw(

     

       225
       225
       +
             "Some of the commits in this PR require the author's and reviewer's attention.",

     

       226
       226
       +
             true,

     

       227
       227
       +
           )

     

       223
       228
        
           core.summary.addEOL()

     

       224
       229
        
       

     

       225
       230
        
           if (results.some(({ type }) => type === 'no-commit-hash')) {

     

       226
       226
       -
             core.summary.addRaw('Please follow the [backporting guidelines](https://github.com/NixOS/nixpkgs/blob/master/CONTRIBUTING.md#how-to-backport-pull-requests) and cherry-pick with the `-x` flag.', true)

     

       227
       227
       -
             core.summary.addRaw('This requires changes to the unstable `master` and `staging` branches first, before backporting them.', true)

     

       231
       231
       +
             core.summary.addRaw(

     

       232
       232
       +
               'Please follow the [backporting guidelines](https://github.com/NixOS/nixpkgs/blob/master/CONTRIBUTING.md#how-to-backport-pull-requests) and cherry-pick with the `-x` flag.',

     

       233
       233
       +
               true,

     

       234
       234
       +
             )

     

       235
       235
       +
             core.summary.addRaw(

     

       236
       236
       +
               'This requires changes to the unstable `master` and `staging` branches first, before backporting them.',

     

       237
       237
       +
               true,

     

       238
       238
       +
             )

     

       228
       239
        
             core.summary.addEOL()

     

       229
       229
       -
             core.summary.addRaw('Occasionally, commits are not cherry-picked at all, for example when updating minor versions of packages which have already advanced to the next major on unstable.', true)

     

       230
       230
       -
             core.summary.addRaw('These commits can optionally be marked with a `Not-cherry-picked-because: <reason>` footer.', true)

     

       240
       240
       +
             core.summary.addRaw(

     

       241
       241
       +
               'Occasionally, commits are not cherry-picked at all, for example when updating minor versions of packages which have already advanced to the next major on unstable.',

     

       242
       242
       +
               true,

     

       243
       243
       +
             )

     

       244
       244
       +
             core.summary.addRaw(

     

       245
       245
       +
               'These commits can optionally be marked with a `Not-cherry-picked-because: <reason>` footer.',

     

       246
       246
       +
               true,

     

       247
       247
       +
             )

     

       231
       248
        
             core.summary.addEOL()

     

       232
       249
        
           }

     

       233
       250
        
       

     

       234
       251
        
           if (results.some(({ type }) => type === 'diff')) {

     

       235
       235
       -
             core.summary.addRaw('Sometimes it is not possible to cherry-pick exactly the same patch.', true)

     

       236
       236
       -
             core.summary.addRaw('This most frequently happens when resolving merge conflicts.', true)

     

       237
       237
       -
             core.summary.addRaw('The range-diff will help to review the resolution of conflicts.', true)

     

       252
       252
       +
             core.summary.addRaw(

     

       253
       253
       +
               'Sometimes it is not possible to cherry-pick exactly the same patch.',

     

       254
       254
       +
               true,

     

       255
       255
       +
             )

     

       256
       256
       +
             core.summary.addRaw(

     

       257
       257
       +
               'This most frequently happens when resolving merge conflicts.',

     

       258
       258
       +
               true,

     

       259
       259
       +
             )

     

       260
       260
       +
             core.summary.addRaw(

     

       261
       261
       +
               'The range-diff will help to review the resolution of conflicts.',

     

       262
       262
       +
               true,

     

       263
       263
       +
             )

     

       238
       264
        
             core.summary.addEOL()

     

       239
       265
        
           }

     

       240
       266
        
       

     

       241
       241
       -
           core.summary.addRaw('If you need to merge this PR despite the warnings, please [dismiss](https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/reviewing-changes-in-pull-requests/dismissing-a-pull-request-review) this review shortly before merging.', true)

     

       267
       267
       +
           core.summary.addRaw(

     

       268
       268
       +
             'If you need to merge this PR despite the warnings, please [dismiss](https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/reviewing-changes-in-pull-requests/dismissing-a-pull-request-review) this review shortly before merging.',

     

       269
       269
       +
             true,

     

       270
       270
       +
           )

     

       242
       271
        
       

     

       243
       272
        
           results.forEach(({ severity, message, diff }) => {

     

       244
       244
       -
             if (severity == 'info') return

     

       273
       273
       +
             if (severity === 'info') return

     

       245
       274
        
       

     

       246
       275
        
             // The docs for markdown alerts only show examples with markdown blockquote syntax, like this:

     

       247
       276
        
             //   > [!WARNING]

     
···

       256
       285
        
             // Whether this is intended or just an implementation detail is unclear.

     

       257
       286
        
             core.summary.addRaw('<blockquote>')

     

       258
       287
        
             core.summary.addRaw(

     

       259
       259
       -
               `\n\n[!${({ important: 'IMPORTANT', warning: 'WARNING', error: 'CAUTION' })[severity]}]`,

     

       288
       288
       +
               `\n\n[!${{ important: 'IMPORTANT', warning: 'WARNING', error: 'CAUTION' }[severity]}]`,

     

       260
       289
        
               true,

     

       261
       290
        
             )

     

       262
       291
        
             core.summary.addRaw(`${message}`, true)

     
···

       305
       334
        
             })

     

       306
       335
        
           ).find(

     

       307
       336
        
             (review) =>

     

       308
       308
       -
               review.user.login == 'github-actions[bot]' &&

     

       337
       337
       +
               review.user.login === 'github-actions[bot]' &&

     

       309
       338
        
               // If a review is still pending, we can just update this instead

     

       310
       339
        
               // of posting a new one.

     

       311
       311
       -
               (review.state == 'CHANGES_REQUESTED' ||

     

       340
       340
       +
               (review.state === 'CHANGES_REQUESTED' ||

     

       312
       341
        
                 // No need to post a new review, if an older one with the exact

     

       313
       342
        
                 // same content had already been dismissed.

     

       314
       314
       -
                 review.body == body),

     

       343
       343
       +
                 review.body === body),

     

       315
       344
        
           )

     

       316
       345
        
       

     

       317
       346
        
           if (dry) {

     

       318
       347
        
             if (pendingReview)

     

       319
       319
       -
               core.info('pending review found: ' + pendingReview.html_url)

     

       348
       348
       +
               core.info(`pending review found: ${pendingReview.html_url}`)

     

       320
       349
        
             else core.info('no pending review found')

     

       321
       350
        
           } else {

     

       322
       351
        
             // Either of those two requests could fail for very long comments. This can only happen

+18 -17

ci/github-script/labels.js

···

       1
       1
       -
       module.exports = async function ({ github, context, core, dry }) {

     

       1
       1
       +
       module.exports = async ({ github, context, core, dry }) => {

     

       2
       2
        
         const path = require('node:path')

     

       3
       3
        
         const { DefaultArtifactClient } = require('@actions/artifact')

     

       4
       4
        
         const { readFile, writeFile } = require('node:fs/promises')

     
···

       27
       27
        
       

     

       28
       28
        
           const approvals = new Set(

     

       29
       29
        
             reviews

     

       30
       30
       -
               .filter((review) => review.state == 'APPROVED')

     

       30
       30
       +
               .filter((review) => review.state === 'APPROVED')

     

       31
       31
        
               .map((review) => review.user?.id),

     

       32
       32
        
           )

     

       33
       33
        
       

     
···

       37
       37
        
           // This is intentionally less than the time that Eval takes, so that the label job

     

       38
       38
        
           // running after Eval can indeed label the PR as conflicted if that is the case.

     

       39
       39
        
           const merge_commit_sha_valid =

     

       40
       40
       -
             new Date() - new Date(pull_request.created_at) > 3 * 60 * 1000

     

       40
       40
       +
             Date.now() - new Date(pull_request.created_at) > 3 * 60 * 1000

     

       41
       41
        
       

     

       42
       42
        
           const prLabels = {

     

       43
       43
        
             // We intentionally don't use the mergeable or mergeable_state attributes.

     
···

       53
       53
        
             // The second pass will then read the result from the first pass and set the label.

     

       54
       54
        
             '2.status: merge conflict':

     

       55
       55
        
               merge_commit_sha_valid && !pull_request.merge_commit_sha,

     

       56
       56
       -
             '12.approvals: 1': approvals.size == 1,

     

       57
       57
       -
             '12.approvals: 2': approvals.size == 2,

     

       56
       56
       +
             '12.approvals: 1': approvals.size === 1,

     

       57
       57
       +
             '12.approvals: 2': approvals.size === 2,

     

       58
       58
        
             '12.approvals: 3+': approvals.size >= 3,

     

       59
       59
        
             '12.first-time contribution': [

     

       60
       60
        
               'NONE',

     
···

       104
       104
        
               // existing reviews, too.

     

       105
       105
        
               '9.needs: reviewer':

     

       106
       106
        
                 !pull_request.draft &&

     

       107
       107
       -
                 pull_request.requested_reviewers.length == 0 &&

     

       108
       108
       -
                 reviews.length == 0,

     

       107
       107
       +
                 pull_request.requested_reviewers.length === 0 &&

     

       108
       108
       +
                 reviews.length === 0,

     

       109
       109
        
             })

     

       110
       110
        
           }

     

       111
       111
        
       

     
···

       125
       125
        
           // called "comparison", yet, will skip the download.

     

       126
       126
        
           const expired =

     

       127
       127
        
             !artifact ||

     

       128
       128
       -
             new Date(artifact?.expires_at ?? 0) <

     

       129
       129
       -
               new Date(new Date().getTime() + 60 * 1000)

     

       128
       128
       +
             new Date(artifact?.expires_at ?? 0) < new Date(Date.now() + 60 * 1000)

     

       130
       129
        
           log('Artifact expires at', artifact?.expires_at ?? '<n/a>')

     

       131
       130
        
           if (!expired) {

     

       132
       131
        
             stats.artifacts++

     
···

       175
       174
        
         async function handle({ item, stats }) {

     

       176
       175
        
           try {

     

       177
       176
        
             const log = (k, v, skip) => {

     

       178
       178
       -
               core.info(`#${item.number} - ${k}: ${v}` + (skip ? ' (skipped)' : ''))

     

       177
       177
       +
               core.info(`#${item.number} - ${k}: ${v}${skip ? ' (skipped)' : ''}`)

     

       179
       178
        
               return skip

     

       180
       179
        
             }

     

       181
       180
        
       

     
···

       257
       256
        
       

     

       258
       257
        
             // No need for an API request, if all labels are the same.

     

       259
       258
        
             const hasChanges = Object.keys(after).some(

     

       260
       260
       -
               (name) => (before[name] ?? false) != after[name],

     

       259
       259
       +
               (name) => (before[name] ?? false) !== after[name],

     

       261
       260
        
             )

     

       262
       261
        
             if (log('Has changes', hasChanges, !hasChanges)) return

     

       263
       262
        
       

     
···

       297
       296
        
                 // Go back as far as the last successful run of this workflow to make sure

     

       298
       297
        
                 // we are not leaving anyone behind on GHA failures.

     

       299
       298
        
                 // Defaults to go back 1 hour on the first run.

     

       300
       300
       -
                 new Date(lastRun?.created_at ?? new Date().getTime() - 1 * 60 * 60 * 1000).getTime(),

     

       299
       299
       +
                 new Date(

     

       300
       300
       +
                   lastRun?.created_at ?? Date.now() - 1 * 60 * 60 * 1000,

     

       301
       301
       +
                 ).getTime(),

     

       301
       302
        
                 // Go back max. 1 day to prevent hitting all API rate limits immediately,

     

       302
       303
        
                 // when GH API returns a wrong workflow by accident.

     

       303
       303
       -
                 new Date().getTime() - 24 * 60 * 60 * 1000,

     

       304
       304
       +
                 Date.now() - 24 * 60 * 60 * 1000,

     

       304
       305
        
               ),

     

       305
       306
        
             )

     

       306
       306
       -
             core.info('cutoff timestamp: ' + cutoff.toISOString())

     

       307
       307
       +
             core.info(`cutoff timestamp: ${cutoff.toISOString()}`)

     

       307
       308
        
       

     

       308
       309
        
             const updatedItems = await github.paginate(

     

       309
       310
        
               github.rest.search.issuesAndPullRequests,

     
···

       400
       401
        
               .concat(updatedItems, allItems.data)

     

       401
       402
        
               .filter(

     

       402
       403
        
                 (thisItem, idx, arr) =>

     

       403
       403
       -
                   idx ==

     

       404
       404
       -
                   arr.findIndex((firstItem) => firstItem.number == thisItem.number),

     

       404
       404
       +
                   idx ===

     

       405
       405
       +
                   arr.findIndex((firstItem) => firstItem.number === thisItem.number),

     

       405
       406
        
               )

     

       406
       407
        
       

     

       407
       408
        
             ;(await Promise.allSettled(items.map((item) => handle({ item, stats }))))

     

       408
       408
       -
               .filter(({ status }) => status == 'rejected')

     

       409
       409
       +
               .filter(({ status }) => status === 'rejected')

     

       409
       410
        
               .map(({ reason }) =>

     

       410
       411
        
                 core.setFailed(`${reason.message}\n${reason.cause.stack}`),

     

       411
       412
        
               )

+1 -1

ci/github-script/prepare.js

···

       1
       1
       -
       module.exports = async function ({ github, context, core }) {

     

       1
       1
       +
       module.exports = async ({ github, context, core }) => {

     

       2
       2
        
         const pull_number = context.payload.pull_request.number

     

       3
       3
        
       

     

       4
       4
        
         for (const retryInterval of [5, 10, 20, 40, 80]) {

+2 -2

ci/github-script/withRateLimit.js

···

       1
       1
       -
       module.exports = async function ({ github, core }, callback) {

     

       1
       1
       +
       module.exports = async ({ github, core }, callback) => {

     

       2
       2
        
         const Bottleneck = require('bottleneck')

     

       3
       3
        
       

     

       4
       4
        
         const stats = {

     
···

       23
       23
        
           // Requests to a different host do not count against the rate limit.

     

       24
       24
        
           if (options.url.startsWith('https://github.com')) return request(options)

     

       25
       25
        
           // Requests to the /rate_limit endpoint do not count against the rate limit.

     

       26
       26
       -
           if (options.url == '/rate_limit') return request(options)

     

       26
       26
       +
           if (options.url === '/rate_limit') return request(options)

     

       27
       27
        
           // Search requests are in a different resource group, which allows 30 requests / minute.

     

       28
       28
        
           // We do less than a handful each run, so not implementing throttling for now.

     

       29
       29
        
           if (options.url.startsWith('/search/')) return request(options)

+6 -2

ci/supportedBranches.js

···

       15
       15
        
       }

     

       16
       16
        
       

     

       17
       17
        
       function split(branch) {

     

       18
       18
       -
         return { ...branch.match(/(?<prefix>.+?)(-(?<version>\d{2}\.\d{2}|unstable)(?:-(?<suffix>.*))?)?$/).groups }

     

       18
       18
       +
         return {

     

       19
       19
       +
           ...branch.match(

     

       20
       20
       +
             /(?<prefix>.+?)(-(?<version>\d{2}\.\d{2}|unstable)(?:-(?<suffix>.*))?)?$/,

     

       21
       21
       +
           ).groups,

     

       22
       22
       +
         }

     

       19
       23
        
       }

     

       20
       24
        
       

     

       21
       25
        
       function classify(branch) {

     

       22
       26
        
         const { prefix, version } = split(branch)

     

       23
       27
        
         return {

     

       24
       28
        
           stable: (version ?? 'unstable') !== 'unstable',

     

       25
       25
       -
           type: typeConfig[prefix] ?? [ 'wip' ]

     

       29
       29
       +
           type: typeConfig[prefix] ?? ['wip'],

     

       26
       30
        
         }

     

       27
       31
        
       }

     

       28
       32

+5 -3

doc/anchor-use.js

···

       1
       1
       -
       document.addEventListener('DOMContentLoaded', function(event) {

     

       2
       2
       -
         anchors.add('h1[id]:not(div.note h1, div.warning h1, div.tip h1, div.caution h1, div.important h1), h2[id]:not(div.note h2, div.warning h2, div.tip h2, div.caution h2, div.important h2), h3[id]:not(div.note h3, div.warning h3, div.tip h3, div.caution h3, div.important h3), h4[id]:not(div.note h4, div.warning h4, div.tip h4, div.caution h4, div.important h4), h5[id]:not(div.note h5, div.warning h5, div.tip h5, div.caution h5, div.important h5), h6[id]:not(div.note h6, div.warning h6, div.tip h6, div.caution h6, div.important h6)');

     

       3
       3
       -
       });

     

       1
       1
       +
       document.addEventListener('DOMContentLoaded', () => {

     

       2
       2
       +
         anchors.add(

     

       3
       3
       +
           'h1[id]:not(div.note h1, div.warning h1, div.tip h1, div.caution h1, div.important h1), h2[id]:not(div.note h2, div.warning h2, div.tip h2, div.caution h2, div.important h2), h3[id]:not(div.note h3, div.warning h3, div.tip h3, div.caution h3, div.important h3), h4[id]:not(div.note h4, div.warning h4, div.tip h4, div.caution h4, div.important h4), h5[id]:not(div.note h5, div.warning h5, div.tip h5, div.caution h5, div.important h5), h6[id]:not(div.note h6, div.warning h6, div.tip h6, div.caution h6, div.important h6)',

     

       4
       4
       +
         )

     

       5
       5
       +
       })

+205 -206

doc/style.css

···

       1
       1
        
       html {

     

       2
       2
       -
           line-height: 1.15;

     

       3
       3
       -
           -webkit-text-size-adjust: 100%;

     

       2
       2
       +
         line-height: 1.15;

     

       3
       3
       +
         -webkit-text-size-adjust: 100%;

     

       4
       4
        
       }

     

       5
       5
        
       

     

       6
       6
        
       body {

     

       7
       7
       -
           margin: 0;

     

       7
       7
       +
         margin: 0;

     

       8
       8
        
       }

     

       9
       9
        
       

     

       10
       10
        
       .book,

     

       11
       11
        
       .appendix {

     

       12
       12
       -
           margin: auto;

     

       13
       13
       -
           width: 100%;

     

       12
       12
       +
         margin: auto;

     

       13
       13
       +
         width: 100%;

     

       14
       14
        
       }

     

       15
       15
        
       

     

       16
       16
        
       @media screen and (min-width: 768px) {

     

       17
       17
       -
           .book,

     

       18
       18
       -
           .appendix {

     

       19
       19
       -
               max-width: 46rem;

     

       20
       20
       -
           }

     

       17
       17
       +
         .book,

     

       18
       18
       +
         .appendix {

     

       19
       19
       +
           max-width: 46rem;

     

       20
       20
       +
         }

     

       21
       21
        
       }

     

       22
       22
        
       

     

       23
       23
        
       @media screen and (min-width: 992px) {

     

       24
       24
       -
           .book,

     

       25
       25
       -
           .appendix {

     

       26
       26
       -
               max-width: 60rem;

     

       27
       27
       -
           }

     

       24
       24
       +
         .book,

     

       25
       25
       +
         .appendix {

     

       26
       26
       +
           max-width: 60rem;

     

       27
       27
       +
         }

     

       28
       28
        
       }

     

       29
       29
        
       

     

       30
       30
        
       @media screen and (min-width: 1200px) {

     

       31
       31
       -
           .book,

     

       32
       32
       -
           .appendix {

     

       33
       33
       -
               max-width: 73rem;

     

       34
       34
       -
           }

     

       31
       31
       +
         .book,

     

       32
       32
       +
         .appendix {

     

       33
       33
       +
           max-width: 73rem;

     

       34
       34
       +
         }

     

       35
       35
        
       }

     

       36
       36
        
       

     

       37
       37
        
       .book .list-of-examples {

     

       38
       38
       -
           display: none;

     

       38
       38
       +
         display: none;

     

       39
       39
        
       }

     

       40
       40
        
       

     

       41
       41
        
       h1 {

     

       42
       42
       -
           font-size: 2em;

     

       43
       43
       -
           margin: 0.67em 0;

     

       42
       42
       +
         font-size: 2em;

     

       43
       43
       +
         margin: 0.67em 0;

     

       44
       44
        
       }

     

       45
       45
        
       

     

       46
       46
        
       hr {

     

       47
       47
       -
           box-sizing: content-box;

     

       48
       48
       -
           height: 0;

     

       49
       49
       -
           overflow: visible;

     

       47
       47
       +
         box-sizing: content-box;

     

       48
       48
       +
         height: 0;

     

       49
       49
       +
         overflow: visible;

     

       50
       50
        
       }

     

       51
       51
        
       

     

       52
       52
        
       pre {

     

       53
       53
       -
           font-family: monospace, monospace;

     

       54
       54
       -
           font-size: 1em;

     

       53
       53
       +
         font-family: monospace;

     

       54
       54
       +
         font-size: 1em;

     

       55
       55
        
       }

     

       56
       56
        
       

     

       57
       57
        
       a {

     

       58
       58
       -
           background-color: transparent;

     

       58
       58
       +
         background-color: transparent;

     

       59
       59
        
       }

     

       60
       60
        
       

     

       61
       61
        
       strong {

     

       62
       62
       -
           font-weight: bolder;

     

       62
       62
       +
         font-weight: bolder;

     

       63
       63
        
       }

     

       64
       64
        
       

     

       65
       65
        
       code {

     

       66
       66
       -
           font-family: monospace, monospace;

     

       67
       67
       -
           font-size: 1em;

     

       66
       66
       +
         font-family: monospace;

     

       67
       67
       +
         font-size: 1em;

     

       68
       68
        
       }

     

       69
       69
        
       

     

       70
       70
        
       sup {

     

       71
       71
       -
           font-size: 75%;

     

       72
       72
       -
           line-height: 0;

     

       73
       73
       -
           position: relative;

     

       74
       74
       -
           vertical-align: baseline;

     

       71
       71
       +
         font-size: 75%;

     

       72
       72
       +
         line-height: 0;

     

       73
       73
       +
         position: relative;

     

       74
       74
       +
         vertical-align: baseline;

     

       75
       75
        
       }

     

       76
       76
        
       

     

       77
       77
        
       sup {

     

       78
       78
       -
           top: -0.5em;

     

       78
       78
       +
         top: -0.5em;

     

       79
       79
        
       }

     

       80
       80
        
       

     

       81
       81
        
       ::-webkit-file-upload-button {

     

       82
       82
       -
           -webkit-appearance: button;

     

       83
       83
       -
           font: inherit;

     

       82
       82
       +
         -webkit-appearance: button;

     

       83
       83
       +
         font: inherit;

     

       84
       84
        
       }

     

       85
       85
        
       

     

       86
       86
        
       pre {

     

       87
       87
       -
           overflow: auto;

     

       87
       87
       +
         overflow: auto;

     

       88
       88
        
       }

     

       89
       89
        
       

     

       90
       90
        
       *,

     

       91
       91
        
       *::before,

     

       92
       92
        
       *::after {

     

       93
       93
       -
           box-sizing: border-box;

     

       93
       93
       +
         box-sizing: border-box;

     

       94
       94
        
       }

     

       95
       95
        
       

     

       96
       96
        
       html {

     

       97
       97
       -
           font-size: 100%;

     

       98
       98
       -
           line-height: 1.77777778;

     

       97
       97
       +
         font-size: 100%;

     

       98
       98
       +
         line-height: 1.77777778;

     

       99
       99
        
       }

     

       100
       100
        
       

     

       101
       101
        
       @media screen and (min-width: 4000px) {

     

       102
       102
       -
           html {

     

       103
       103
       -
               background: #000;

     

       104
       104
       -
           }

     

       102
       102
       +
         html {

     

       103
       103
       +
           background: #000;

     

       104
       104
       +
         }

     

       105
       105
        
       

     

       106
       106
       -
           html body {

     

       107
       107
       -
               margin: auto;

     

       108
       108
       -
               max-width: 250rem;

     

       109
       109
       -
           }

     

       106
       106
       +
         html body {

     

       107
       107
       +
           margin: auto;

     

       108
       108
       +
           max-width: 250rem;

     

       109
       109
       +
         }

     

       110
       110
        
       }

     

       111
       111
        
       

     

       112
       112
        
       @media screen and (max-width: 320px) {

     

       113
       113
       -
           html {

     

       114
       114
       -
               font-size: calc(16 / 320 * 100vw);

     

       115
       115
       -
           }

     

       113
       113
       +
         html {

     

       114
       114
       +
           font-size: calc(16 / 320 * 100vw);

     

       115
       115
       +
         }

     

       116
       116
        
       }

     

       117
       117
        
       

     

       118
       118
        
       body {

     

       119
       119
       -
           font-size: 1rem;

     

       120
       120
       -
           font-family: "Roboto", sans-serif;

     

       121
       121
       -
           font-weight: 300;

     

       122
       122
       -
           color: var(--main-text-color);

     

       123
       123
       -
           background-color: var(--background);

     

       124
       124
       -
           min-height: 100vh;

     

       125
       125
       -
           display: flex;

     

       126
       126
       -
           flex-direction: column;

     

       119
       119
       +
         font-size: 1rem;

     

       120
       120
       +
         font-family: "Roboto", sans-serif;

     

       121
       121
       +
         font-weight: 300;

     

       122
       122
       +
         color: var(--main-text-color);

     

       123
       123
       +
         background-color: var(--background);

     

       124
       124
       +
         min-height: 100vh;

     

       125
       125
       +
         display: flex;

     

       126
       126
       +
         flex-direction: column;

     

       127
       127
        
       }

     

       128
       128
        
       

     

       129
       129
        
       @media screen and (max-width: 767.9px) {

     

       130
       130
       -
           body {

     

       131
       131
       -
               padding-left: 1rem;

     

       132
       132
       -
               padding-right: 1rem;

     

       133
       133
       -
           }

     

       130
       130
       +
         body {

     

       131
       131
       +
           padding-left: 1rem;

     

       132
       132
       +
           padding-right: 1rem;

     

       133
       133
       +
         }

     

       134
       134
        
       }

     

       135
       135
        
       

     

       136
       136
        
       a {

     

       137
       137
       -
           text-decoration: none;

     

       138
       138
       -
           border-bottom: 1px solid;

     

       139
       139
       -
           color: var(--link-color);

     

       137
       137
       +
         text-decoration: none;

     

       138
       138
       +
         border-bottom: 1px solid;

     

       139
       139
       +
         color: var(--link-color);

     

       140
       140
        
       }

     

       141
       141
        
       

     

       142
       142
        
       ul {

     

       143
       143
       -
           padding: 0;

     

       144
       144
       -
           margin-top: 0;

     

       145
       145
       -
           margin-right: 0;

     

       146
       146
       -
           margin-bottom: 1rem;

     

       147
       147
       -
           margin-left: 1rem;

     

       143
       143
       +
         padding: 0;

     

       144
       144
       +
         margin-top: 0;

     

       145
       145
       +
         margin-right: 0;

     

       146
       146
       +
         margin-bottom: 1rem;

     

       147
       147
       +
         margin-left: 1rem;

     

       148
       148
        
       }

     

       149
       149
        
       

     

       150
       150
        
       table {

     

       151
       151
       -
           border-collapse: collapse;

     

       152
       152
       -
           width: 100%;

     

       153
       153
       -
           margin-bottom: 1rem;

     

       151
       151
       +
         border-collapse: collapse;

     

       152
       152
       +
         width: 100%;

     

       153
       153
       +
         margin-bottom: 1rem;

     

       154
       154
        
       }

     

       155
       155
        
       

     

       156
       156
        
       thead th {

     

       157
       157
       -
           text-align: left;

     

       157
       157
       +
         text-align: left;

     

       158
       158
        
       }

     

       159
       159
        
       

     

       160
       160
        
       hr {

     

       161
       161
       -
           margin-top: 1rem;

     

       162
       162
       -
           margin-bottom: 1rem;

     

       161
       161
       +
         margin-top: 1rem;

     

       162
       162
       +
         margin-bottom: 1rem;

     

       163
       163
        
       }

     

       164
       164
        
       

     

       165
       165
        
       h1 {

     

       166
       166
       -
           font-weight: 800;

     

       167
       167
       -
           line-height: 110%;

     

       168
       168
       -
           font-size: 200%;

     

       169
       169
       -
           margin-bottom: 1rem;

     

       170
       170
       -
           color: var(--heading-color);

     

       166
       166
       +
         font-weight: 800;

     

       167
       167
       +
         line-height: 110%;

     

       168
       168
       +
         font-size: 200%;

     

       169
       169
       +
         margin-bottom: 1rem;

     

       170
       170
       +
         color: var(--heading-color);

     

       171
       171
        
       }

     

       172
       172
        
       

     

       173
       173
        
       h2 {

     

       174
       174
       -
           font-weight: 800;

     

       175
       175
       -
           line-height: 110%;

     

       176
       176
       -
           font-size: 170%;

     

       177
       177
       -
           margin-bottom: 0.625rem;

     

       178
       178
       -
           color: var(--heading-color);

     

       174
       174
       +
         font-weight: 800;

     

       175
       175
       +
         line-height: 110%;

     

       176
       176
       +
         font-size: 170%;

     

       177
       177
       +
         margin-bottom: 0.625rem;

     

       178
       178
       +
         color: var(--heading-color);

     

       179
       179
        
       }

     

       180
       180
        
       

     

       181
       181
        
       h2:not(:first-child) {

     

       182
       182
       -
           margin-top: 1rem;

     

       182
       182
       +
         margin-top: 1rem;

     

       183
       183
        
       }

     

       184
       184
        
       

     

       185
       185
        
       h3 {

     

       186
       186
       -
           font-weight: 800;

     

       187
       187
       -
           line-height: 110%;

     

       188
       188
       -
           margin-bottom: 1rem;

     

       189
       189
       -
           font-size: 150%;

     

       190
       190
       -
           color: var(--heading-color);

     

       186
       186
       +
         font-weight: 800;

     

       187
       187
       +
         line-height: 110%;

     

       188
       188
       +
         margin-bottom: 1rem;

     

       189
       189
       +
         font-size: 150%;

     

       190
       190
       +
         color: var(--heading-color);

     

       191
       191
        
       }

     

       192
       192
        
       

     

       193
       193
        
       .note h3,

     
···

       195
       195
        
       .warning h3,

     

       196
       196
        
       .caution h3,

     

       197
       197
        
       .important h3 {

     

       198
       198
       -
           font-size: 120%;

     

       198
       198
       +
         font-size: 120%;

     

       199
       199
        
       }

     

       200
       200
        
       

     

       201
       201
        
       h4 {

     

       202
       202
       -
           font-weight: 800;

     

       203
       203
       -
           line-height: 110%;

     

       204
       204
       -
           margin-bottom: 1rem;

     

       205
       205
       -
           font-size: 140%;

     

       206
       206
       -
           color: var(--heading-color);

     

       202
       202
       +
         font-weight: 800;

     

       203
       203
       +
         line-height: 110%;

     

       204
       204
       +
         margin-bottom: 1rem;

     

       205
       205
       +
         font-size: 140%;

     

       206
       206
       +
         color: var(--heading-color);

     

       207
       207
        
       }

     

       208
       208
        
       

     

       209
       209
        
       h5 {

     

       210
       210
       -
           font-weight: 800;

     

       211
       211
       -
           line-height: 110%;

     

       212
       212
       -
           margin-bottom: 1rem;

     

       213
       213
       -
           font-size: 130%;

     

       214
       214
       -
           color: var(--small-heading-color);

     

       210
       210
       +
         font-weight: 800;

     

       211
       211
       +
         line-height: 110%;

     

       212
       212
       +
         margin-bottom: 1rem;

     

       213
       213
       +
         font-size: 130%;

     

       214
       214
       +
         color: var(--small-heading-color);

     

       215
       215
        
       }

     

       216
       216
        
       

     

       217
       217
        
       h6 {

     

       218
       218
       -
           font-weight: 800;

     

       219
       219
       -
           line-height: 110%;

     

       220
       220
       -
           margin-bottom: 1rem;

     

       221
       221
       -
           font-size: 120%;

     

       218
       218
       +
         font-weight: 800;

     

       219
       219
       +
         line-height: 110%;

     

       220
       220
       +
         margin-bottom: 1rem;

     

       221
       221
       +
         font-size: 120%;

     

       222
       222
        
       }

     

       223
       223
        
       

     

       224
       224
        
       strong {

     

       225
       225
       -
           font-weight: bold;

     

       225
       225
       +
         font-weight: bold;

     

       226
       226
        
       }

     

       227
       227
        
       

     

       228
       228
        
       p {

     

       229
       229
       -
           margin-top: 0;

     

       230
       230
       -
           margin-bottom: 1rem;

     

       229
       229
       +
         margin-top: 0;

     

       230
       230
       +
         margin-bottom: 1rem;

     

       231
       231
        
       }

     

       232
       232
        
       

     

       233
       233
        
       dt > *:first-child,

     

       234
       234
        
       dd > *:first-child {

     

       235
       235
       -
           margin-top: 0;

     

       235
       235
       +
         margin-top: 0;

     

       236
       236
        
       }

     

       237
       237
        
       

     

       238
       238
        
       dt > *:last-child,

     

       239
       239
        
       dd > *:last-child {

     

       240
       240
       -
           margin-bottom: 0;

     

       240
       240
       +
         margin-bottom: 0;

     

       241
       241
        
       }

     

       242
       242
        
       

     

       243
       243
        
       pre,

     

       244
       244
        
       code {

     

       245
       245
       -
           font-family: monospace;

     

       245
       245
       +
         font-family: monospace;

     

       246
       246
        
       }

     

       247
       247
        
       

     

       248
       248
        
       code {

     

       249
       249
       -
           color: #ff8657;

     

       250
       250
       -
           background: #f4f4f4;

     

       251
       251
       -
           display: inline-block;

     

       252
       252
       -
           padding: 0 0.5rem;

     

       253
       253
       -
           border: 1px solid #d8d8d8;

     

       254
       254
       -
           border-radius: 0.5rem;

     

       255
       255
       -
           line-height: 1.57777778;

     

       249
       249
       +
         color: #ff8657;

     

       250
       250
       +
         background: #f4f4f4;

     

       251
       251
       +
         display: inline-block;

     

       252
       252
       +
         padding: 0 0.5rem;

     

       253
       253
       +
         border: 1px solid #d8d8d8;

     

       254
       254
       +
         border-radius: 0.5rem;

     

       255
       255
       +
         line-height: 1.57777778;

     

       256
       256
        
       }

     

       257
       257
        
       

     

       258
       258
        
       div.book .programlisting,

     

       259
       259
        
       div.appendix .programlisting {

     

       260
       260
       -
           border-radius: 0.5rem;

     

       261
       261
       -
           padding: 1rem;

     

       262
       262
       -
           overflow: auto;

     

       263
       263
       -
           background: var(--codeblock-background);

     

       264
       264
       -
           color: var(--codeblock-text-color);

     

       260
       260
       +
         border-radius: 0.5rem;

     

       261
       261
       +
         padding: 1rem;

     

       262
       262
       +
         overflow: auto;

     

       263
       263
       +
         background: var(--codeblock-background);

     

       264
       264
       +
         color: var(--codeblock-text-color);

     

       265
       265
        
       }

     

       266
       266
        
       

     

       267
       267
        
       div.book .note,

     
···

       274
       274
        
       div.appendix .warning,

     

       275
       275
        
       div.appendix .caution,

     

       276
       276
        
       div.appendix .important {

     

       277
       277
       -
           margin-bottom: 1rem;

     

       278
       278
       -
           border-radius: 0.5rem;

     

       279
       279
       -
           padding: 1.5rem;

     

       280
       280
       -
           overflow: auto;

     

       281
       281
       -
           background: #f4f4f4;

     

       277
       277
       +
         margin-bottom: 1rem;

     

       278
       278
       +
         border-radius: 0.5rem;

     

       279
       279
       +
         padding: 1.5rem;

     

       280
       280
       +
         overflow: auto;

     

       281
       281
       +
         background: #f4f4f4;

     

       282
       282
        
       }

     

       283
       283
        
       

     

       284
       284
        
       div.book .note > .title,

     
···

       291
       291
        
       div.appendix .warning > .title,

     

       292
       292
        
       div.appendix .caution > .title,

     

       293
       293
        
       div.appendix .important > .title {

     

       294
       294
       -
           font-weight: 800;

     

       295
       295
       -
           line-height: 110%;

     

       296
       296
       -
           margin-bottom: 1rem;

     

       297
       297
       -
           color: inherit;

     

       298
       298
       -
           margin-bottom: 0;

     

       294
       294
       +
         font-weight: 800;

     

       295
       295
       +
         line-height: 110%;

     

       296
       296
       +
         color: inherit;

     

       297
       297
       +
         margin-bottom: 0;

     

       299
       298
        
       }

     

       300
       299
        
       

     

       301
       300
        
       div.book .note > :first-child,

     
···

       308
       307
        
       div.appendix .warning > :first-child,

     

       309
       308
        
       div.appendix .caution > :first-child,

     

       310
       309
        
       div.appendix .important > :first-child {

     

       311
       311
       -
           margin-top: 0;

     

       310
       310
       +
         margin-top: 0;

     

       312
       311
        
       }

     

       313
       312
        
       

     

       314
       313
        
       div.book .note > :last-child,

     
···

       321
       320
        
       div.appendix .warning > :last-child,

     

       322
       321
        
       div.appendix .caution > :last-child,

     

       323
       322
        
       div.appendix .important > :last-child {

     

       324
       324
       -
           margin-bottom: 0;

     

       323
       323
       +
         margin-bottom: 0;

     

       325
       324
        
       }

     

       326
       325
        
       

     

       327
       326
        
       div.book .note,

     

       328
       327
        
       div.book .tip,

     

       329
       328
        
       div.appendix .note,

     

       330
       329
        
       div.appendix .tip {

     

       331
       331
       -
           color: var(--note-text-color);

     

       332
       332
       -
           background: var(--note-background);

     

       330
       330
       +
         color: var(--note-text-color);

     

       331
       331
       +
         background: var(--note-background);

     

       333
       332
        
       }

     

       334
       333
        
       

     

       335
       334
        
       div.book .warning,

     

       336
       335
        
       div.book .caution,

     

       337
       336
        
       div.appendix .warning,

     

       338
       337
        
       div.appendix .caution {

     

       339
       339
       -
           color: var(--warning-text-color);

     

       340
       340
       -
           background-color: var(--warning-background);

     

       338
       338
       +
         color: var(--warning-text-color);

     

       339
       339
       +
         background-color: var(--warning-background);

     

       341
       340
        
       }

     

       342
       341
        
       

     

       343
       342
        
       div.book .section,

     

       344
       343
        
       div.appendix .section {

     

       345
       345
       -
           margin-top: 2em;

     

       344
       344
       +
         margin-top: 2em;

     

       346
       345
        
       }

     

       347
       346
        
       

     

       348
       347
        
       div.book div.example,

     

       349
       348
        
       div.appendix div.example {

     

       350
       350
       -
           margin-top: 1.5em;

     

       349
       349
       +
         margin-top: 1.5em;

     

       351
       350
        
       }

     

       352
       351
        
       

     

       353
       352
        
       div.book div.example details,

     

       354
       353
        
       div.appendix div.example details {

     

       355
       355
       -
           padding: 5px;

     

       354
       354
       +
         padding: 5px;

     

       356
       355
        
       }

     

       357
       356
        
       

     

       358
       357
        
       div.book div.example details[open],

     

       359
       358
        
       div.appendix div.example details[open] {

     

       360
       360
       -
           border: 1px solid #aaa;

     

       361
       361
       -
           border-radius: 4px;

     

       359
       359
       +
         border: 1px solid #aaa;

     

       360
       360
       +
         border-radius: 4px;

     

       362
       361
        
       }

     

       363
       362
        
       

     

       364
       363
        
       div.book div.example details > summary,

     

       365
       364
        
       div.appendix div.example details > summary {

     

       366
       366
       -
           cursor: pointer;

     

       365
       365
       +
         cursor: pointer;

     

       367
       366
        
       }

     

       368
       367
        
       

     

       369
       368
        
       div.book br.example-break,

     

       370
       369
        
       div.appendix br.example-break {

     

       371
       371
       -
           display: none;

     

       370
       370
       +
         display: none;

     

       372
       371
        
       }

     

       373
       372
        
       

     

       374
       373
        
       div.book div.footnotes > hr,

     

       375
       374
        
       div.appendix div.footnotes > hr {

     

       376
       376
       -
           border-color: #d8d8d8;

     

       375
       375
       +
         border-color: #d8d8d8;

     

       377
       376
        
       }

     

       378
       377
        
       

     

       379
       378
        
       div.book div.footnotes > br,

     

       380
       379
        
       div.appendix div.footnotes > br {

     

       381
       381
       -
           display: none;

     

       380
       380
       +
         display: none;

     

       382
       381
        
       }

     

       383
       382
        
       

     

       384
       383
        
       div.book dt,

     

       385
       384
        
       div.appendix dt {

     

       386
       386
       -
           margin-top: 1em;

     

       385
       385
       +
         margin-top: 1em;

     

       387
       386
        
       }

     

       388
       387
        
       

     

       389
       388
        
       div.book .toc dt,

     

       390
       389
        
       div.appendix .toc dt {

     

       391
       391
       -
           margin-top: 0;

     

       390
       390
       +
         margin-top: 0;

     

       392
       391
        
       }

     

       393
       392
        
       

     

       394
       393
        
       div.book .list-of-examples dt,

     

       395
       394
        
       div.appendix .list-of-examples dt {

     

       396
       396
       -
           margin-top: 0;

     

       395
       395
       +
         margin-top: 0;

     

       397
       396
        
       }

     

       398
       397
        
       

     

       399
       398
        
       div.book code,

     

       400
       399
        
       div.appendix code {

     

       401
       401
       -
           padding: 0;

     

       402
       402
       -
           border: 0;

     

       403
       403
       -
           background-color: inherit;

     

       404
       404
       -
           color: inherit;

     

       405
       405
       -
           font-size: 100%;

     

       406
       406
       -
           -webkit-hyphens: none;

     

       407
       407
       -
           -moz-hyphens: none;

     

       408
       408
       -
           hyphens: none;

     

       400
       400
       +
         padding: 0;

     

       401
       401
       +
         border: 0;

     

       402
       402
       +
         background-color: inherit;

     

       403
       403
       +
         color: inherit;

     

       404
       404
       +
         font-size: 100%;

     

       405
       405
       +
         -webkit-hyphens: none;

     

       406
       406
       +
         -moz-hyphens: none;

     

       407
       407
       +
         hyphens: none;

     

       409
       408
        
       }

     

       410
       409
        
       

     

       411
       410
        
       div.book div.toc,

     

       412
       411
        
       div.appendix div.toc {

     

       413
       413
       -
           margin-bottom: 3em;

     

       414
       414
       -
           border-bottom: 0.0625rem solid #d8d8d8;

     

       412
       412
       +
         margin-bottom: 3em;

     

       413
       413
       +
         border-bottom: 0.0625rem solid #d8d8d8;

     

       415
       414
        
       }

     

       416
       415
        
       

     

       417
       416
        
       div.book div.toc dd,

     

       418
       417
        
       div.appendix div.toc dd {

     

       419
       419
       -
           margin-left: 2em;

     

       418
       418
       +
         margin-left: 2em;

     

       420
       419
        
       }

     

       421
       420
        
       

     

       422
       421
        
       div.book span.command,

     

       423
       422
        
       div.appendix span.command {

     

       424
       424
       -
           font-family: monospace;

     

       425
       425
       -
           -webkit-hyphens: none;

     

       426
       426
       -
           -moz-hyphens: none;

     

       427
       427
       -
           hyphens: none;

     

       423
       423
       +
         font-family: monospace;

     

       424
       424
       +
         -webkit-hyphens: none;

     

       425
       425
       +
         -moz-hyphens: none;

     

       426
       426
       +
         hyphens: none;

     

       428
       427
        
       }

     

       429
       428
        
       

     

       430
       429
        
       div.book .informaltable th,

     

       431
       430
        
       div.book .informaltable td,

     

       432
       431
        
       div.appendix .informaltable th,

     

       433
       432
        
       div.appendix .informaltable td {

     

       434
       434
       -
           padding: 0.5rem;

     

       433
       433
       +
         padding: 0.5rem;

     

       435
       434
        
       }

     

       436
       435
        
       

     

       437
       436
        
       div.book .variablelist .term,

     

       438
       437
        
       div.appendix .variablelist .term {

     

       439
       439
       -
           font-weight: 500;

     

       438
       438
       +
         font-weight: 500;

     

       440
       439
        
       }

     

       441
       440
        
       

     

       442
       441
        
       /*

     
···

       444
       443
        
         For more details, see https://highlightjs.readthedocs.io/en/latest/css-classes-reference.html#stylable-scopes

     

       445
       444
        
       */

     

       446
       445
        
       .hljs-meta.prompt_ {

     

       447
       447
       -
           user-select: none;

     

       448
       448
       -
           -webkit-user-select: none;

     

       446
       446
       +
         user-select: none;

     

       447
       447
       +
         -webkit-user-select: none;

     

       449
       448
        
       }

     

       450
       449
        
       

     

       451
       450
        
       :root {

     

       452
       452
       -
           --background: #fff;

     

       453
       453
       -
           --main-text-color: #000;

     

       454
       454
       -
           --link-color: #405d99;

     

       455
       455
       -
           --heading-color: #6586c8;

     

       456
       456
       -
           --small-heading-color: #6a6a6a;

     

       457
       457
       -
           --note-text-color: #5277c3;

     

       458
       458
       -
           --note-background: #f2f8fd;

     

       459
       459
       -
           --warning-text-color: #cc3900;

     

       460
       460
       -
           --warning-background: #fff5e1;

     

       461
       461
       -
           --codeblock-background: #f2f8fd;

     

       462
       462
       -
           --codeblock-text-color: #000;

     

       451
       451
       +
         --background: #fff;

     

       452
       452
       +
         --main-text-color: #000;

     

       453
       453
       +
         --link-color: #405d99;

     

       454
       454
       +
         --heading-color: #6586c8;

     

       455
       455
       +
         --small-heading-color: #6a6a6a;

     

       456
       456
       +
         --note-text-color: #5277c3;

     

       457
       457
       +
         --note-background: #f2f8fd;

     

       458
       458
       +
         --warning-text-color: #cc3900;

     

       459
       459
       +
         --warning-background: #fff5e1;

     

       460
       460
       +
         --codeblock-background: #f2f8fd;

     

       461
       461
       +
         --codeblock-text-color: #000;

     

       463
       462
        
       }

     

       464
       463
        
       

     

       465
       464
        
       @media (prefers-color-scheme: dark) {

     

       466
       466
       -
           :root {

     

       467
       467
       -
               --background: #242424;

     

       468
       468
       -
               --main-text-color: #fff;

     

       469
       469
       -
               --link-color: #6586c8;

     

       470
       470
       -
               --small-heading-color: #fff;

     

       471
       471
       -
               --note-background: none;

     

       472
       472
       -
               --warning-background: none;

     

       473
       473
       -
               --codeblock-background: #393939;

     

       474
       474
       -
               --codeblock-text-color: #fff;

     

       475
       475
       -
           }

     

       465
       465
       +
         :root {

     

       466
       466
       +
           --background: #242424;

     

       467
       467
       +
           --main-text-color: #fff;

     

       468
       468
       +
           --link-color: #6586c8;

     

       469
       469
       +
           --small-heading-color: #fff;

     

       470
       470
       +
           --note-background: none;

     

       471
       471
       +
           --warning-background: none;

     

       472
       472
       +
           --codeblock-background: #393939;

     

       473
       473
       +
           --codeblock-text-color: #fff;

     

       474
       474
       +
         }

     

       476
       475
        
       

     

       477
       477
       -
           div.book .note,

     

       478
       478
       -
           div.book .tip,

     

       479
       479
       -
           div.appendix .note,

     

       480
       480
       -
           div.appendix .tip,

     

       481
       481
       -
           div.book .warning,

     

       482
       482
       -
           div.book .caution,

     

       483
       483
       -
           div.appendix .warning,

     

       484
       484
       -
           div.appendix .caution {

     

       485
       485
       -
               border: 2px solid;

     

       486
       486
       -
               font-weight: 400;

     

       487
       487
       -
           }

     

       476
       476
       +
         div.book .note,

     

       477
       477
       +
         div.book .tip,

     

       478
       478
       +
         div.appendix .note,

     

       479
       479
       +
         div.appendix .tip,

     

       480
       480
       +
         div.book .warning,

     

       481
       481
       +
         div.book .caution,

     

       482
       482
       +
         div.appendix .warning,

     

       483
       483
       +
         div.appendix .caution {

     

       484
       484
       +
           border: 2px solid;

     

       485
       485
       +
           font-weight: 400;

     

       486
       486
       +
         }

     

       488
       487
        
       }

     

       489
       488
        
       

     

       490
       489
        
       @font-face {

     

       491
       491
       -
           font-family: Roboto;

     

       492
       492
       -
           src: url(Roboto.ttf);

     

       490
       490
       +
         font-family: Roboto;

     

       491
       491
       +
         src: url(Roboto.ttf);

     

       493
       492
        
       }